{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
module MAlonzo.Code.Data.Tree.AVL where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.DifferenceList
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Tree.AVL.Height
import qualified MAlonzo.Code.Data.Tree.AVL.Indexed
import qualified MAlonzo.Code.Data.Tree.AVL.Value
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict
d_K'38'__106 :: p -> p -> p -> p -> p -> p -> ()
d_K'38'__106 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Tree_112 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_Tree_112 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
d_Value_114 :: p -> p -> p -> p -> p -> ()
d_Value_114 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
d_const_120 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
d_const_120 :: () -> () -> () -> T_StrictTotalOrder_1036 -> () -> () -> T_Value_38
d_const_120 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 = () -> () -> T_Value_38
du_const_120
du_const_120 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_120 :: () -> () -> T_Value_38
du_const_120 ()
v0 ()
v1
= T_Value_38 -> T_Value_38
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94
d_fromPair_128 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
d_fromPair_128 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_128 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 = () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_128
du_fromPair_128 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
du_fromPair_128 :: () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_128 ()
v0 T_Value_38
v1 T_Σ_14
v2
= (T_Σ_14 -> T_K'38'__56) -> T_Σ_14 -> T_K'38'__56
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_86 T_Σ_14
v2
d_toPair_182 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_182 :: T_K'38'__56 -> T_Σ_14
d_toPair_182 T_K'38'__56
v0
= (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0))
((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0))
d_key_204 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_204 :: T_K'38'__56 -> Any
d_key_204 T_K'38'__56
v0
= (T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0)
d_value_206 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_206 :: T_K'38'__56 -> Any
d_value_206 T_K'38'__56
v0
= (T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0)
d_family_216 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_216 :: T_Value_38 -> Any -> ()
d_family_216 = T_Value_38 -> Any -> ()
forall a. a
erased
d_respects_218 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_218 :: T_Value_38 -> Any -> Any -> Any -> Any -> Any
d_respects_218 T_Value_38
v0
= (T_Value_38 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Value_38 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v0)
d_Tree_254 :: p -> p -> p -> p -> p -> p -> ()
d_Tree_254 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Tree_254
= C_tree_262 Integer MAlonzo.Code.Data.Tree.AVL.Indexed.T_Tree_180
d_Val_272 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_272 :: T_Value_38 -> Any -> ()
d_Val_272 = T_Value_38 -> Any -> ()
forall a. a
erased
d_empty_274 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> T_Tree_254
d_empty_274 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
d_empty_274 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 = T_Tree_254
du_empty_274
du_empty_274 :: T_Tree_254
du_empty_274 :: T_Tree_254
du_empty_274
= let v0 :: t
v0 = (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Tree_254
C_tree_262 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) in
Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any
forall a b. a -> b
coe
Any
forall a. a
v0
((T__'60''8314'__20 -> T_Tree_180) -> Any -> Any
forall a b. a -> b
coe
T__'60''8314'__20 -> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_192
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))
d_singleton_278 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> T_Tree_254
d_singleton_278 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> Any
-> T_Tree_254
d_singleton_278 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 Any
v6 Any
v7
= Any -> Any -> T_Tree_254
du_singleton_278 Any
v6 Any
v7
du_singleton_278 :: AgdaAny -> AgdaAny -> T_Tree_254
du_singleton_278 :: Any -> Any -> T_Tree_254
du_singleton_278 Any
v0 Any
v1
= (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Tree_254
C_tree_262 (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
((Any -> Any -> T_Σ_14 -> T_Tree_180) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14 -> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_singleton_798 (Any -> Any
forall a b. a -> b
coe Any
v0)
(Any -> Any
forall a b. a -> b
coe Any
v1)
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))
d_insert_286 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
d_insert_286 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
d_insert_286 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any
v6 Any
v7 T_Tree_254
v8
= T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any
v6 Any
v7 T_Tree_254
v8
du_insert_286 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_insert_286 :: T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Any
v3 T_Tree_254
v4
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v4 of
C_tree_262 Integer
v5 T_Tree_180
v6
-> let v7 :: t
v7
= (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
((T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14)
-> T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> Any
-> T_Tree_180
-> Any
-> Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_920 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Any
v3 T_Tree_180
v6
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))))
(Integer -> Any
forall a b. a -> b
coe Integer
v5)) in
Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any
forall a b. a -> b
coe
Any
forall a. a
v7
(T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
((T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14)
-> T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> Any
-> T_Tree_180
-> Any
-> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_920 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Any
v3 T_Tree_180
v6
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))))
T_Tree_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
d_insertWith_296 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
d_insertWith_296 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
d_insertWith_296 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any
v6 Maybe Any -> Any
v7 T_Tree_254
v8
= T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
du_insertWith_296 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any
v6 Maybe Any -> Any
v7 T_Tree_254
v8
du_insertWith_296 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
du_insertWith_296 :: T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
du_insertWith_296 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Maybe Any -> Any
v3 T_Tree_254
v4
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v4 of
C_tree_262 Integer
v5 T_Tree_180
v6
-> let v7 :: t
v7
= (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
((T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_818 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (Any -> Any
forall a b. a -> b
coe Any
v2) ((Maybe Any -> Any) -> Any
forall a b. a -> b
coe Maybe Any -> Any
v3) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v6)
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))))
(Integer -> Any
forall a b. a -> b
coe Integer
v5)) in
Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any
forall a b. a -> b
coe
Any
forall a. a
v7
(T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
((T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_818 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (Any -> Any
forall a b. a -> b
coe Any
v2) ((Maybe Any -> Any) -> Any
forall a b. a -> b
coe Maybe Any -> Any
v3) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v6)
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))))
T_Tree_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
d_delete_304 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_254 -> T_Tree_254
d_delete_304 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> T_Tree_254
-> T_Tree_254
d_delete_304 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 Any
v6 T_Tree_254
v7 = T_StrictTotalOrder_1036 -> Any -> T_Tree_254 -> T_Tree_254
du_delete_304 T_StrictTotalOrder_1036
v3 Any
v6 T_Tree_254
v7
du_delete_304 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
AgdaAny -> T_Tree_254 -> T_Tree_254
du_delete_304 :: T_StrictTotalOrder_1036 -> Any -> T_Tree_254 -> T_Tree_254
du_delete_304 T_StrictTotalOrder_1036
v0 Any
v1 T_Tree_254
v2
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v2 of
C_tree_262 Integer
v3 T_Tree_180
v4
-> let v5 :: t
v5
= (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
((T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Integer
-> Any
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Integer
-> Any
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_936 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
(Any -> Any
forall a b. a -> b
coe Any
v1) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v4)
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))))
(Integer -> Any
forall a b. a -> b
coe Integer
v3)) in
Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any
forall a b. a -> b
coe
Any
forall a. a
v5
(T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
((T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Integer
-> Any
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Integer
-> Any
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_936 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
(Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
(Any -> Any
forall a b. a -> b
coe Any
v1) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v4)
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))))
T_Tree_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
d_lookup_312 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> AgdaAny -> Maybe AgdaAny
d_lookup_312 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Any
-> Maybe Any
d_lookup_312 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 T_Tree_254
v6 Any
v7
= T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 T_StrictTotalOrder_1036
v3 T_Value_38
v5 T_Tree_254
v6 Any
v7
du_lookup_312 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> AgdaAny -> Maybe AgdaAny
du_lookup_312 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Tree_254
v2 Any
v3
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v2 of
C_tree_262 Integer
v4 T_Tree_180
v5
-> (T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> Any -> T_Σ_14 -> Maybe Any)
-> Any -> Any -> Any -> Any -> Any -> Maybe Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> Any -> T_Σ_14 -> Maybe Any
MAlonzo.Code.Data.Tree.AVL.Indexed.du_lookup_1034 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)
(T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v5) (Any -> Any
forall a b. a -> b
coe Any
v3)
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))
T_Tree_254
_ -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_330 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_330 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Val_330 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
d_Wal_332 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_332 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Wal_332 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
d_map_334 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
d_map_334 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
d_map_334 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 ~T_Value_38
v7 Any -> Any -> Any
v8 T_Tree_254
v9 = (Any -> Any -> Any) -> T_Tree_254 -> T_Tree_254
du_map_334 Any -> Any -> Any
v8 T_Tree_254
v9
du_map_334 ::
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
du_map_334 :: (Any -> Any -> Any) -> T_Tree_254 -> T_Tree_254
du_map_334 Any -> Any -> Any
v0 T_Tree_254
v1
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v1 of
C_tree_262 Integer
v2 T_Tree_180
v3
-> (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Tree_254
C_tree_262 (Integer -> Any
forall a b. a -> b
coe Integer
v2)
(((Any -> Any -> Any) -> T_Tree_180 -> T_Tree_180)
-> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_Tree_180 -> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_map_1188 ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any
v0) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v3))
T_Tree_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_348 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_348 :: T_Value_38 -> Any -> ()
d_Val_348 = T_Value_38 -> Any -> ()
forall a. a
erased
d_member_350 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_254 -> Bool
d_member_350 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> T_Tree_254
-> Bool
d_member_350 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any
v6 T_Tree_254
v7
= T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du_member_350 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any
v6 T_Tree_254
v7
du_member_350 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_254 -> Bool
du_member_350 :: T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du_member_350 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 T_Tree_254
v3
= (Maybe Any -> Bool) -> Any -> Bool
forall a b. a -> b
coe
Maybe Any -> Bool
MAlonzo.Code.Data.Maybe.Base.du_is'45'just_20
((T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v3) (Any -> Any
forall a b. a -> b
coe Any
v2))
d_headTail_356 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_356 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Maybe T_Σ_14
d_headTail_356 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_headTail_356 T_StrictTotalOrder_1036
v3 T_Tree_254
v6
du_headTail_356 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_356 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_headTail_356 T_StrictTotalOrder_1036
v0 T_Tree_254
v1
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v1 of
C_tree_262 Integer
v2 T_Tree_180
v3
-> let v4 :: b
v4
= let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> b
forall a b. a -> b
coe
(let v5 :: t
v5
= (Integer -> T_Tree_180 -> T_Σ_14) -> Any -> Any -> t
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_headTail_648 (Integer -> Any
forall a b. a -> b
coe Integer
v4)
(T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v3) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Σ_14
forall a b. a -> b
coe Any
forall a. a
v5 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v6 Any
v7
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v8 Any
v9
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v9 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v10 Any
v11
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(Any -> Any
forall a b. a -> b
coe Any
v6)
((Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(Any -> Any
forall a b. a -> b
coe Any
v10) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
((T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'737'_290
(T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe Any -> Any
forall a b. a -> b
coe
Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
(Any -> Any
forall a b. a -> b
coe Any
v6))))
(Maybe Any -> Any
forall a b. a -> b
coe
Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> Any
forall a b. a -> b
coe
T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
(Any -> Any
forall a b. a -> b
coe Any
v11))))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
Any -> Maybe T_Σ_14
forall a b. a -> b
coe
(case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v3 of
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_192 T__'60''8314'__20
v5
-> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
T_Tree_180
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
T_Tree_254
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_initLast_368 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_368 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Maybe T_Σ_14
d_initLast_368 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_initLast_368 T_StrictTotalOrder_1036
v3 T_Tree_254
v6
du_initLast_368 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_368 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_initLast_368 T_StrictTotalOrder_1036
v0 T_Tree_254
v1
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v1 of
C_tree_262 Integer
v2 T_Tree_180
v3
-> let v4 :: b
v4
= let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> b
forall a b. a -> b
coe
(let v5 :: t
v5
= (Integer -> T_Tree_180 -> T_Σ_14) -> Any -> Any -> t
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_initLast_698 (Integer -> Any
forall a b. a -> b
coe Integer
v4)
(T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v3) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Σ_14
forall a b. a -> b
coe Any
forall a. a
v5 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v6 Any
v7
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v8 Any
v9
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v9 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v10 Any
v11
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(Any -> Any
forall a b. a -> b
coe Any
v10) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
((T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'691'_316
(T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe Any -> Any
forall a b. a -> b
coe
Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe
T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
(Any -> Any
forall a b. a -> b
coe Any
v6))))
(Maybe Any -> Any
forall a b. a -> b
coe
Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
(Any -> Any
forall a b. a -> b
coe Any
v11)
(T__'60''8314'__20 -> Any
forall a b. a -> b
coe
T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))
(Any -> Any
forall a b. a -> b
coe Any
v6))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
Any -> Maybe T_Σ_14
forall a b. a -> b
coe
(case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v3 of
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_192 T__'60''8314'__20
v5
-> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
T_Tree_180
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
T_Tree_254
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_foldr_382 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> T_Tree_254 -> AgdaAny
d_foldr_382 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> ()
-> ()
-> (Any -> Any -> Any -> Any)
-> Any
-> T_Tree_254
-> Any
d_foldr_382 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 ~()
v6 ~()
v7 Any -> Any -> Any -> Any
v8 Any
v9 T_Tree_254
v10
= (Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382 Any -> Any -> Any -> Any
v8 Any
v9 T_Tree_254
v10
du_foldr_382 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> T_Tree_254 -> AgdaAny
du_foldr_382 :: (Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382 Any -> Any -> Any -> Any
v0 Any
v1 T_Tree_254
v2
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v2 of
C_tree_262 Integer
v3 T_Tree_180
v4
-> ((Any -> Any -> Any -> Any) -> Any -> T_Tree_180 -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> T_Tree_180 -> Any
MAlonzo.Code.Data.Tree.AVL.Indexed.du_foldr_1114 ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v0) (Any -> Any
forall a b. a -> b
coe Any
v1)
(T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v4)
T_Tree_254
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromList_390 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] -> T_Tree_254
d_fromList_390 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> [T_K'38'__56]
-> T_Tree_254
d_fromList_390 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_1036
-> T_Value_38 -> [T_K'38'__56] -> T_Tree_254
du_fromList_390 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_fromList_390 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] -> T_Tree_254
du_fromList_390 :: T_StrictTotalOrder_1036
-> T_Value_38 -> [T_K'38'__56] -> T_Tree_254
du_fromList_390 T_StrictTotalOrder_1036
v0 T_Value_38
v1
= ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> [T_K'38'__56] -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
(((Any -> Any) -> (Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Function.Base.du__'8728''8242'__216
(((Any -> Any -> Any) -> T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_Σ_14 -> Any
MAlonzo.Code.Data.Product.Base.du_uncurry_244
((T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254)
-> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)))
((T_K'38'__56 -> T_Σ_14) -> Any
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80))
(T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
du_empty_274)
d_toList_392 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_392 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> [T_K'38'__56]
d_toList_392 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_Tree_254 -> [T_K'38'__56]
du_toList_392 T_Tree_254
v6
du_toList_392 ::
T_Tree_254 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_392 :: T_Tree_254 -> [T_K'38'__56]
du_toList_392 T_Tree_254
v0
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v0 of
C_tree_262 Integer
v1 T_Tree_180
v2
-> (([Any] -> [Any]) -> [Any]) -> Any -> [T_K'38'__56]
forall a b. a -> b
coe
([Any] -> [Any]) -> [Any]
MAlonzo.Code.Data.DifferenceList.du_toList_54
((T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]) -> Any -> Any
forall a b. a -> b
coe
T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
MAlonzo.Code.Data.Tree.AVL.Indexed.du_toDiffList_1140 (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v2))
T_Tree_254
_ -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_size_396 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> Integer
d_size_396 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Integer
d_size_396 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_Tree_254 -> Integer
du_size_396 T_Tree_254
v6
du_size_396 :: T_Tree_254 -> Integer
du_size_396 :: T_Tree_254 -> Integer
du_size_396 T_Tree_254
v0
= case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v0 of
C_tree_262 Integer
v1 T_Tree_180
v2
-> (T_Tree_180 -> Integer) -> T_Tree_180 -> Integer
forall a b. a -> b
coe T_Tree_180 -> Integer
MAlonzo.Code.Data.Tree.AVL.Indexed.du_size_1164 T_Tree_180
v2
T_Tree_254
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_412 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_412 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Val_412 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
d_Wal_414 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_414 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Wal_414 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
d_unionWith_418 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_unionWith_418 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_unionWith_418 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 T_Value_38
v7 Any -> Any -> Maybe Any -> Any
v8 T_Tree_254
v9 T_Tree_254
v10
= T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 T_StrictTotalOrder_1036
v3 T_Value_38
v7 Any -> Any -> Maybe Any -> Any
v8 T_Tree_254
v9 T_Tree_254
v10
du_unionWith_418 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_unionWith_418 :: T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any -> Any -> Maybe Any -> Any
v2 T_Tree_254
v3 T_Tree_254
v4
= ((Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v5 Any
v6 ->
(T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
du_insertWith_296 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (Any -> Any
forall a b. a -> b
coe Any
v5) ((Any -> Any -> Maybe Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Maybe Any -> Any
v2 Any
v5 Any
v6)))
(T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v4) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v3)
d_Val_438 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_438 :: T_Value_38 -> Any -> ()
d_Val_438 = T_Value_38 -> Any -> ()
forall a. a
erased
d_union_440 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_union_440 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_union_440 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_440 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_union_440 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_440 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_440 T_StrictTotalOrder_1036
v0 T_Value_38
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254)
-> Any -> Any -> Any -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
d_unionsWith_444 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[T_Tree_254] -> T_Tree_254
d_unionsWith_444 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
d_unionsWith_444 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any -> Any -> Maybe Any -> Any
v6 [T_Tree_254]
v7
= T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_444 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any -> Any -> Maybe Any -> Any
v6 [T_Tree_254]
v7
du_unionsWith_444 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[T_Tree_254] -> T_Tree_254
du_unionsWith_444 :: T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_444 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any -> Any -> Maybe Any -> Any
v2 [T_Tree_254]
v3
= ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
((T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Maybe Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Maybe Any -> Any
v2))
(T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
du_empty_274) ([T_Tree_254] -> Any
forall a b. a -> b
coe [T_Tree_254]
v3)
d_unions_450 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_254] -> T_Tree_254
d_unions_450 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> [T_Tree_254]
-> T_Tree_254
d_unions_450 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_unions_450 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_unions_450 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_254] -> T_Tree_254
du_unions_450 :: T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_unions_450 T_StrictTotalOrder_1036
v0 T_Value_38
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254)
-> Any -> Any -> Any -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_444 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
d_Val_468 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_468 :: T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
d_Val_468 = T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
forall a. a
erased
d_Wal_470 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_470 :: T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
d_Wal_470 = T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
forall a. a
erased
d_Xal_472 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Xal_472 :: T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
d_Xal_472 = T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
forall a. a
erased
d_intersectionWith_476 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_intersectionWith_476 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_intersectionWith_476 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 T_Tree_254
v11
T_Tree_254
v12
= T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 T_StrictTotalOrder_1036
v3 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 T_Tree_254
v11 T_Tree_254
v12
du_intersectionWith_476 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersectionWith_476 :: T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Value_38
v2 Any -> Any -> Any -> Any
v3 T_Tree_254
v4 T_Tree_254
v5
= ((Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382
((T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
du_cons_490 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v2) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v3) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v5))
(T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
du_empty_274) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v4)
d_cons_490 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
T_Tree_254 ->
T_Tree_254 -> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
d_cons_490 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
d_cons_490 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 ~T_Tree_254
v11 T_Tree_254
v12 Any
v13
Any
v14
= T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
du_cons_490 T_StrictTotalOrder_1036
v3 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 T_Tree_254
v12 Any
v13 Any
v14
du_cons_490 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
T_Tree_254 -> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_cons_490 :: T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
du_cons_490 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Value_38
v2 Any -> Any -> Any -> Any
v3 T_Tree_254
v4 Any
v5 Any
v6
= let v7 :: t
v7 = (T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any)
-> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v4) (Any -> Any
forall a b. a -> b
coe Any
v5) in
Any -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe
(case Any -> Maybe Any
forall a b. a -> b
coe Any
forall a. a
v7 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v8
-> (T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(((Any -> Any -> Any -> Any -> Any) -> T_Value_38)
-> (Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(Any -> Any -> Any -> Any -> Any) -> T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.C_MkValue_50
(T_Value_38 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> T_Value_38
forall a b. a -> b
coe T_Value_38
v2)))
(Any -> Any
forall a b. a -> b
coe Any
v5) ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v3 Any
v5 Any
v6 Any
v8)
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> (Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v8 -> Any
v8)
Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_Val_508 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_508 :: T_Value_38 -> Any -> ()
d_Val_508 = T_Value_38 -> Any -> ()
forall a. a
erased
d_intersection_510 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_intersection_510 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_intersection_510 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5
= T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_510 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_intersection_510 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_510 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_510 T_StrictTotalOrder_1036
v0 T_Value_38
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254)
-> Any
-> Any
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
d_intersectionsWith_514 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[T_Tree_254] -> T_Tree_254
d_intersectionsWith_514 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
d_intersectionsWith_514 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any -> Any -> Any -> Any
v6 [T_Tree_254]
v7
= T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_intersectionsWith_514 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any -> Any -> Any -> Any
v6 [T_Tree_254]
v7
du_intersectionsWith_514 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[T_Tree_254] -> T_Tree_254
du_intersectionsWith_514 :: T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_intersectionsWith_514 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any -> Any -> Any -> Any
v2 [T_Tree_254]
v3
= case [T_Tree_254] -> [Any]
forall a b. a -> b
coe [T_Tree_254]
v3 of
[] -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
du_empty_274
(:) Any
v4 [Any]
v5
-> ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldl_230
((T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v2))
(Any -> Any
forall a b. a -> b
coe Any
v4) ([Any] -> Any
forall a b. a -> b
coe [Any]
v5)
[Any]
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
d_intersections_524 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_254] -> T_Tree_254
d_intersections_524 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> [T_Tree_254]
-> T_Tree_254
d_intersections_524 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5
= T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_intersections_524 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_intersections_524 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_254] -> T_Tree_254
du_intersections_524 :: T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_intersections_524 T_StrictTotalOrder_1036
v0 T_Value_38
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254)
-> Any -> Any -> Any -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_intersectionsWith_514 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
d__'8712''63'__530 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_254 -> Bool
d__'8712''63'__530 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> T_Tree_254
-> Bool
d__'8712''63'__530 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5
= T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du__'8712''63'__530 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du__'8712''63'__530 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_254 -> Bool
du__'8712''63'__530 :: T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du__'8712''63'__530 T_StrictTotalOrder_1036
v0 T_Value_38
v1 = (T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> T_Tree_254 -> Bool)
-> Any -> Any -> Any -> T_Tree_254 -> Bool
forall a b. a -> b
coe T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du_member_350 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)