{-# 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
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'__92 :: p -> p -> p -> p -> p -> p -> ()
d_K'38'__92 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Tree_98 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_Tree_98 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
d_Value_100 :: p -> p -> p -> p -> p -> ()
d_Value_100 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
d_const_106 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
d_const_106 :: () -> () -> () -> T_StrictTotalOrder_864 -> () -> () -> T_Value_38
d_const_106 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 = () -> () -> T_Value_38
du_const_106
du_const_106 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_106 :: () -> () -> T_Value_38
du_const_106 ()
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_114 ::
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_864 ->
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_114 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_114 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 = () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_114
du_fromPair_114 ::
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_114 :: () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_114 ()
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_168 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_168 :: T_K'38'__56 -> T_Σ_14
d_toPair_168 = (T_K'38'__56 -> T_Σ_14) -> T_K'38'__56 -> T_Σ_14
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80
d_key_190 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_190 :: T_K'38'__56 -> AgdaAny
d_key_190 T_K'38'__56
v0
= (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
d_value_192 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_192 :: T_K'38'__56 -> AgdaAny
d_value_192 T_K'38'__56
v0
= (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
d_family_202 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_202 :: T_Value_38 -> AgdaAny -> ()
d_family_202 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_respects_204 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_204 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_204 T_Value_38
v0
= (T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v0)
d_Tree_240 :: p -> p -> p -> p -> p -> p -> ()
d_Tree_240 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Tree_240
= C_tree_248 Integer MAlonzo.Code.Data.Tree.AVL.Indexed.T_Tree_166
d_Val_258 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_258 :: T_Value_38 -> AgdaAny -> ()
d_Val_258 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_empty_260 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> T_Tree_240
d_empty_260 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
d_empty_260 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 = T_Tree_240
du_empty_260
du_empty_260 :: T_Tree_240
du_empty_260 :: T_Tree_240
du_empty_260
= let v0 :: t
v0 = (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Tree_240
C_tree_248 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)) in
AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v0
((T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'60''8314'__20 -> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_178
(T__'60''8314'__20 -> AgdaAny
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_264 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> T_Tree_240
d_singleton_264 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_240
d_singleton_264 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 AgdaAny
v6 AgdaAny
v7
= AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_264 AgdaAny
v6 AgdaAny
v7
du_singleton_264 :: AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_264 :: AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_264 AgdaAny
v0 AgdaAny
v1
= (Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Tree_240
C_tree_248 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer))
((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_singleton_784 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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_272 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
d_insert_272 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_insert_272 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 AgdaAny
v7 T_Tree_240
v8
= T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 AgdaAny
v7 T_Tree_240
v8
du_insert_272 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_240
v4
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v4 of
C_tree_248 Integer
v5 T_Tree_166
v6
-> let v7 :: t
v7
= (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
((T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_906 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_166
v6
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe Integer
v5)) in
AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v7
(T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
((T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_906 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_166
v6
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
d_insertWith_282 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
d_insertWith_282 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
d_insertWith_282 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 Maybe AgdaAny -> AgdaAny
v7 T_Tree_240
v8
= T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_282 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 Maybe AgdaAny -> AgdaAny
v7 T_Tree_240
v8
du_insertWith_282 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_insertWith_282 :: T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_282 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_240
v4
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v4 of
C_tree_248 Integer
v5 T_Tree_166
v6
-> let v7 :: t
v7
= (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
((T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe Integer
v5)) in
AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v7
(T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
((T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
d_delete_290 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_240 -> T_Tree_240
d_delete_290 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_delete_290 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7 = T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_290 T_StrictTotalOrder_864
v3 AgdaAny
v6 T_Tree_240
v7
du_delete_290 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_290 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_290 T_StrictTotalOrder_864
v0 AgdaAny
v1 T_Tree_240
v2
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v2 of
C_tree_248 Integer
v3 T_Tree_166
v4
-> let v5 :: t
v5
= (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v4)
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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 -> AgdaAny
forall a b. a -> b
coe Integer
v3)) in
AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
forall a. a
v5
(T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v4)
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
d_lookup_298 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_240 -> Maybe AgdaAny
d_lookup_298 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> T_Tree_240
-> Maybe AgdaAny
d_lookup_298 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
= T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
du_lookup_298 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 T_Tree_240
v3
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v3 of
C_tree_248 Integer
v4 T_Tree_166
v5
-> (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
MAlonzo.Code.Data.Tree.AVL.Indexed.du_lookup_1020 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v5)
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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 -> AgdaAny
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_240
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_316 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_316 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Val_316 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_Wal_318 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_318 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Wal_318 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_map_320 ::
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_864 ->
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_240 -> T_Tree_240
d_map_320 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
d_map_320 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 ~T_Value_38
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_240
v9 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_320 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_240
v9
du_map_320 ::
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_320 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_320 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_240
v1
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v1 of
C_tree_248 Integer
v2 T_Tree_166
v3
-> (Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Tree_240
C_tree_248 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
(((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_map_1174 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v3))
T_Tree_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_334 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_334 :: T_Value_38 -> AgdaAny -> ()
d_Val_334 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d__'8712''63'__336 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_240 -> Bool
d__'8712''63'__336 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> T_Tree_240
-> Bool
d__'8712''63'__336 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
= T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__336 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
du__'8712''63'__336 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__336 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__336 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 T_Tree_240
v3
= (Maybe AgdaAny -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
Maybe AgdaAny -> Bool
MAlonzo.Code.Data.Maybe.Base.du_is'45'just_20
((T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v3))
d_headTail_342 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_342 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> Maybe T_Σ_14
d_headTail_342 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_headTail_342 T_StrictTotalOrder_864
v3 T_Tree_240
v6
du_headTail_342 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_342 :: T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_headTail_342 T_StrictTotalOrder_864
v0 T_Tree_240
v1
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v1 of
C_tree_248 Integer
v2 T_Tree_166
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
AgdaAny -> b
forall a b. a -> b
coe
(let v5 :: t
v5
= (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
(T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v3) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
-> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
((Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'737'_276
(T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
(T__'60''8331'__20 -> AgdaAny
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))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11))))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
(case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_178 T__'60''8314'__20
v5
-> Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)
T_Tree_240
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_initLast_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_356 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> Maybe T_Σ_14
d_initLast_356 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_initLast_356 T_StrictTotalOrder_864
v3 T_Tree_240
v6
du_initLast_356 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_356 :: T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_initLast_356 T_StrictTotalOrder_864
v0 T_Tree_240
v1
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v1 of
C_tree_248 Integer
v2 T_Tree_166
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
AgdaAny -> b
forall a b. a -> b
coe
(let v5 :: t
v5
= (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_initLast_684 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
(T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v3) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
-> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'691'_302
(T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
(T__'60''8314'__20 -> AgdaAny
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)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
(case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_178 T__'60''8314'__20
v5
-> Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)
T_Tree_240
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_foldr_372 ::
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_864 ->
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_240 -> AgdaAny
d_foldr_372 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_240
-> AgdaAny
d_foldr_372 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 T_Tree_240
v10
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 T_Tree_240
v10
du_foldr_372 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_240
v2
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v2 of
C_tree_248 Integer
v3 T_Tree_166
v4
-> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Indexed.du_foldr_1100 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
(T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v4)
T_Tree_240
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromList_380 ::
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_864 ->
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_240
d_fromList_380 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> [T_K'38'__56]
-> T_Tree_240
d_fromList_380 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_864 -> T_Value_38 -> [T_K'38'__56] -> T_Tree_240
du_fromList_380 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_fromList_380 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] -> T_Tree_240
du_fromList_380 :: T_StrictTotalOrder_864 -> T_Value_38 -> [T_K'38'__56] -> T_Tree_240
du_fromList_380 T_StrictTotalOrder_864
v0 T_Value_38
v1
= ((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_K'38'__56] -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
(((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
(((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.du_uncurry_264
((T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1)))
((T_K'38'__56 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80))
(T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
du_empty_260)
d_toList_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_382 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> [T_K'38'__56]
d_toList_382 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_Tree_240 -> [T_K'38'__56]
du_toList_382 T_Tree_240
v6
du_toList_382 ::
T_Tree_240 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_382 :: T_Tree_240 -> [T_K'38'__56]
du_toList_382 T_Tree_240
v0
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v0 of
C_tree_248 Integer
v1 T_Tree_166
v2
-> (([AgdaAny] -> [AgdaAny]) -> [AgdaAny]) -> AgdaAny -> [T_K'38'__56]
forall a b. a -> b
coe
([AgdaAny] -> [AgdaAny]) -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du_toList_54
((T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
MAlonzo.Code.Data.Tree.AVL.Indexed.du_toDiffList_1126 (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v2))
T_Tree_240
_ -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_size_386 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> Integer
d_size_386 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> Integer
d_size_386 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_Tree_240 -> Integer
du_size_386 T_Tree_240
v6
du_size_386 :: T_Tree_240 -> Integer
du_size_386 :: T_Tree_240 -> Integer
du_size_386 T_Tree_240
v0
= case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v0 of
C_tree_248 Integer
v1 T_Tree_166
v2
-> (T_Tree_166 -> Integer) -> T_Tree_166 -> Integer
forall a b. a -> b
coe T_Tree_166 -> Integer
MAlonzo.Code.Data.Tree.AVL.Indexed.du_size_1150 T_Tree_166
v2
T_Tree_240
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_402 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_402 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Val_402 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_Wal_404 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_404 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Wal_404 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_unionWith_408 ::
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_864 ->
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_240 -> T_Tree_240 -> T_Tree_240
d_unionWith_408 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_unionWith_408 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 T_Value_38
v7 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v8 T_Tree_240
v9 T_Tree_240
v10
= T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 T_StrictTotalOrder_864
v3 T_Value_38
v7 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v8 T_Tree_240
v9 T_Tree_240
v10
du_unionWith_408 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_unionWith_408 :: T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 T_Tree_240
v3 T_Tree_240
v4
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v5 AgdaAny
v6 ->
(T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_282 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)))
(T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v4) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v3)
d_Val_428 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_428 :: T_Value_38 -> AgdaAny -> ()
d_Val_428 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_union_430 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> T_Tree_240 -> T_Tree_240
d_union_430 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_union_430 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_430 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_union_430 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_430 :: T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_430 T_StrictTotalOrder_864
v0 T_Value_38
v1
= (T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
d_unionsWith_434 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[T_Tree_240] -> T_Tree_240
d_unionsWith_434 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
d_unionsWith_434 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
= T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_434 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
du_unionsWith_434 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[T_Tree_240] -> T_Tree_240
du_unionsWith_434 :: T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_434 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 [T_Tree_240]
v3
= ((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
((T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2))
(T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
du_empty_260) ([T_Tree_240] -> AgdaAny
forall a b. a -> b
coe [T_Tree_240]
v3)
d_unions_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_240] -> T_Tree_240
d_unions_440 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> [T_Tree_240]
-> T_Tree_240
d_unions_440 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_unions_440 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_unions_440 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_240] -> T_Tree_240
du_unions_440 :: T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_unions_440 T_StrictTotalOrder_864
v0 T_Value_38
v1
= (T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_240] -> T_Tree_240
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_434 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
d_Val_458 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_458 :: T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
d_Val_458 = T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
forall a. a
erased
d_Wal_460 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_460 :: T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
d_Wal_460 = T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
forall a. a
erased
d_Xal_462 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_462 :: T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
d_Xal_462 = T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
forall a. a
erased
d_intersectionWith_466 ::
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_864 ->
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_240 -> T_Tree_240 -> T_Tree_240
d_intersectionWith_466 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_intersectionWith_466 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_240
v11
T_Tree_240
v12
= T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 T_StrictTotalOrder_864
v3 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_240
v11 T_Tree_240
v12
du_intersectionWith_466 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersectionWith_466 :: T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 T_StrictTotalOrder_864
v0 T_Value_38
v1 T_Value_38
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Tree_240
v4 T_Tree_240
v5
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372
((T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
du_cons_480 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v5))
(T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
du_empty_260) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v4)
d_cons_480 ::
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_864 ->
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_240 ->
T_Tree_240 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
d_cons_480 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_cons_480 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Tree_240
v11 T_Tree_240
v12 AgdaAny
v13
AgdaAny
v14
= T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
du_cons_480 T_StrictTotalOrder_864
v3 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_240
v12 AgdaAny
v13 AgdaAny
v14
du_cons_480 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
T_Tree_240 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_cons_480 :: T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
du_cons_480 T_StrictTotalOrder_864
v0 T_Value_38
v1 T_Value_38
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Tree_240
v4 AgdaAny
v5 AgdaAny
v6
= let v7 :: t
v7 = (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v4) in
AgdaAny -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe
(case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v8
-> (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v8 -> AgdaAny
v8)
Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_Val_498 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_498 :: T_Value_38 -> AgdaAny -> ()
d_Val_498 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
d_intersection_500 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> T_Tree_240 -> T_Tree_240
d_intersection_500 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_intersection_500 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5
= T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_500 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_intersection_500 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_500 :: T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_500 T_StrictTotalOrder_864
v0 T_Value_38
v1
= (T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
d_intersectionsWith_504 ::
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[T_Tree_240] -> T_Tree_240
d_intersectionsWith_504 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
d_intersectionsWith_504 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
= T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_intersectionsWith_504 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
du_intersectionsWith_504 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
[T_Tree_240] -> T_Tree_240
du_intersectionsWith_504 :: T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_intersectionsWith_504 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 [T_Tree_240]
v3
= case [T_Tree_240] -> [AgdaAny]
forall a b. a -> b
coe [T_Tree_240]
v3 of
[] -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
du_empty_260
(:) AgdaAny
v4 [AgdaAny]
v5
-> ((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldl_254
((T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5)
[AgdaAny]
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
d_intersections_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_240] -> T_Tree_240
d_intersections_514 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> [T_Tree_240]
-> T_Tree_240
d_intersections_514 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5
= T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_intersections_514 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_intersections_514 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
[T_Tree_240] -> T_Tree_240
du_intersections_514 :: T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_intersections_514 T_StrictTotalOrder_864
v0 T_Value_38
v1
= (T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_240] -> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_intersectionsWith_504 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))