{-# 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.Map 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
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
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
d_Tree_42 :: p -> p -> p -> p -> p -> p -> ()
d_Tree_42 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Map_194 ::
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 -> () -> ()
d_Map_194 :: () -> () -> () -> T_StrictTotalOrder_1036 -> () -> () -> ()
d_Map_194 = () -> () -> () -> T_StrictTotalOrder_1036 -> () -> () -> ()
forall a. a
erased
d_empty_198 ::
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.T_Tree_254
d_empty_198 :: () -> () -> () -> T_StrictTotalOrder_1036 -> () -> () -> T_Tree_254
d_empty_198 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_Tree_254
du_empty_198
du_empty_198 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_empty_198 :: T_Tree_254
du_empty_198 = T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_empty_274
d_singleton_200 ::
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 ->
() -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_singleton_200 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> T_Tree_254
d_singleton_200 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = AgdaAny -> AgdaAny -> T_Tree_254
du_singleton_200
du_singleton_200 ::
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_singleton_200 :: AgdaAny -> AgdaAny -> T_Tree_254
du_singleton_200 = (AgdaAny -> AgdaAny -> T_Tree_254)
-> AgdaAny -> AgdaAny -> T_Tree_254
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_singleton_278
d_insert_202 ::
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 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_insert_202 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> T_Tree_254
-> T_Tree_254
d_insert_202 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036
-> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_insert_202 T_StrictTotalOrder_1036
v3
du_insert_202 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_insert_202 :: T_StrictTotalOrder_1036
-> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_insert_202 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_254
-> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_insert_286 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.C_MkValue_50
(\ AgdaAny
v1 AgdaAny
v2 -> let v3 :: p -> p
v3 = \ p
v3 -> p
v3 in (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny -> AgdaAny
forall {p}. p -> p
v3)))
d_insertWith_204 ::
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 ->
() ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_insertWith_204 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
d_insertWith_204 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
du_insertWith_204 T_StrictTotalOrder_1036
v3
du_insertWith_204 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_insertWith_204 :: T_StrictTotalOrder_1036
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
du_insertWith_204 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_insertWith_296 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.C_MkValue_50
(\ AgdaAny
v1 AgdaAny
v2 -> let v3 :: p -> p
v3 = \ p
v3 -> p
v3 in (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny -> AgdaAny
forall {p}. p -> p
v3)))
d_delete_206 ::
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 ->
() ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_delete_206 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> AgdaAny
-> T_Tree_254
-> T_Tree_254
d_delete_206 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_delete_206 T_StrictTotalOrder_1036
v3
du_delete_206 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_delete_206 :: T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_delete_206 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> T_Tree_254)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_delete_304 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
d_lookup_208 ::
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.T_Tree_254 -> AgdaAny -> Maybe AgdaAny
d_lookup_208 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Tree_254
-> AgdaAny
-> Maybe AgdaAny
d_lookup_208 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> T_Tree_254 -> AgdaAny -> Maybe AgdaAny
du_lookup_208 T_StrictTotalOrder_1036
v3
du_lookup_208 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> AgdaAny -> Maybe AgdaAny
du_lookup_208 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> AgdaAny -> Maybe AgdaAny
du_lookup_208 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Tree.AVL.du_lookup_312 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_map_210 ::
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 ->
() ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_map_210 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
d_map_210 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny
v8 = (AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
du_map_210 AgdaAny -> AgdaAny
v8
du_map_210 ::
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_map_210 :: (AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
du_map_210 AgdaAny -> AgdaAny
v0
= ((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254)
-> AgdaAny -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_map_334 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny -> AgdaAny
v0))
d_member_214 ::
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 ->
() -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> Bool
d_member_214 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> AgdaAny
-> T_Tree_254
-> Bool
d_member_214 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> Bool
du_member_214 T_StrictTotalOrder_1036
v3
du_member_214 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> Bool
du_member_214 :: T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> Bool
du_member_214 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38 -> AgdaAny -> T_Tree_254 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_254 -> Bool
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> AgdaAny -> T_Tree_254 -> Bool
MAlonzo.Code.Data.Tree.AVL.du_member_350 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_headTail_216 ::
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.T_Tree_254 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_216 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Tree_254
-> Maybe T_Σ_14
d_headTail_216 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_headTail_216 T_StrictTotalOrder_1036
v3
du_headTail_216 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_216 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_headTail_216 T_StrictTotalOrder_1036
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> Maybe T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
(((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_64
(((AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8321'_138
((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_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
MAlonzo.Code.Data.Tree.AVL.du_headTail_356 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0))
d_initLast_218 ::
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.T_Tree_254 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_218 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Tree_254
-> Maybe T_Σ_14
d_initLast_218 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_initLast_218 T_StrictTotalOrder_1036
v3
du_initLast_218 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_218 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_initLast_218 T_StrictTotalOrder_1036
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> Maybe T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
(((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_64
(((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8322'_150
((AgdaAny -> T_K'38'__56 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80))))
((T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
MAlonzo.Code.Data.Tree.AVL.du_initLast_368 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0))
d_foldr_220 ::
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 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> AgdaAny
d_foldr_220 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_254
-> AgdaAny
d_foldr_220 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_254 -> AgdaAny
du_foldr_220 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8
du_foldr_220 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> AgdaAny
du_foldr_220 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_254 -> AgdaAny
du_foldr_220 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_254 -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_254 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.du_foldr_382 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1))
d_fromList_226 ::
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.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_fromList_226 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> [T_Σ_14]
-> T_Tree_254
d_fromList_226 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> [T_Σ_14] -> T_Tree_254
du_fromList_226 T_StrictTotalOrder_1036
v3
du_fromList_226 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_fromList_226 :: T_StrictTotalOrder_1036 -> [T_Σ_14] -> T_Tree_254
du_fromList_226 T_StrictTotalOrder_1036
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_Σ_14] -> T_Tree_254
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
((T_StrictTotalOrder_1036
-> T_Value_38 -> [T_K'38'__56] -> T_Tree_254)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> [T_K'38'__56] -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_fromList_390 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94))
(((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
((T_Σ_14 -> T_K'38'__56) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_86))
d_toList_228 ::
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.T_Tree_254 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
d_toList_228 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Tree_254
-> [T_Σ_14]
d_toList_228 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_Tree_254 -> [T_Σ_14]
du_toList_228
du_toList_228 ::
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
du_toList_228 :: T_Tree_254 -> [T_Σ_14]
du_toList_228
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> [T_Σ_14]
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
(((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
((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_254 -> [T_K'38'__56]) -> AgdaAny
forall a b. a -> b
coe T_Tree_254 -> [T_K'38'__56]
MAlonzo.Code.Data.Tree.AVL.du_toList_392)
d_size_230 ::
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.T_Tree_254 -> Integer
d_size_230 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Tree_254
-> Integer
d_size_230 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_Tree_254 -> Integer
du_size_230
du_size_230 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> Integer
du_size_230 :: T_Tree_254 -> Integer
du_size_230 = (T_Tree_254 -> Integer) -> T_Tree_254 -> Integer
forall a b. a -> b
coe T_Tree_254 -> Integer
MAlonzo.Code.Data.Tree.AVL.du_size_396
d_unionWith_232 ::
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 ->
() ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_unionWith_232 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_unionWith_232 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> Maybe AgdaAny -> AgdaAny
v8
= T_StrictTotalOrder_1036
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_232 T_StrictTotalOrder_1036
v3 AgdaAny -> Maybe AgdaAny -> AgdaAny
v8
du_unionWith_232 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_unionWith_232 :: T_StrictTotalOrder_1036
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_232 T_StrictTotalOrder_1036
v0 AgdaAny -> Maybe AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_unionWith_418 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v1))
d_union_236 ::
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.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_union_236 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_union_236 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_236 T_StrictTotalOrder_1036
v3
du_union_236 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_union_236 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_236 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_union_440 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_unionsWith_238 ::
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 ->
() ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_unionsWith_238 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254
d_unionsWith_238 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 AgdaAny -> Maybe AgdaAny -> AgdaAny
v6
= T_StrictTotalOrder_1036
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_238 T_StrictTotalOrder_1036
v3 AgdaAny -> Maybe AgdaAny -> AgdaAny
v6
du_unionsWith_238 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_unionsWith_238 :: T_StrictTotalOrder_1036
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_238 T_StrictTotalOrder_1036
v0 AgdaAny -> Maybe AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_unionsWith_444 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v1))
d_unions_242 ::
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.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_unions_242 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> [T_Tree_254]
-> T_Tree_254
d_unions_242 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> [T_Tree_254] -> T_Tree_254
du_unions_242 T_StrictTotalOrder_1036
v3
du_unions_242 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_unions_242 :: T_StrictTotalOrder_1036 -> [T_Tree_254] -> T_Tree_254
du_unions_242 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38 -> [T_Tree_254] -> T_Tree_254)
-> AgdaAny -> AgdaAny -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_unions_450 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_intersectionWith_244 ::
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 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_intersectionWith_244 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_intersectionWith_244 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9 AgdaAny -> AgdaAny -> AgdaAny
v10
= T_StrictTotalOrder_1036
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_244 T_StrictTotalOrder_1036
v3 AgdaAny -> AgdaAny -> AgdaAny
v10
du_intersectionWith_244 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_intersectionWith_244 :: T_StrictTotalOrder_1036
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_244 T_StrictTotalOrder_1036
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_intersectionWith_476 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny
v1))
d_intersection_248 ::
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.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_intersection_248 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_intersection_248 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_248 T_StrictTotalOrder_1036
v3
du_intersection_248 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_intersection_248 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_248 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_intersection_510 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_intersectionsWith_250 ::
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 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_intersectionsWith_250 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254
d_intersectionsWith_250 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 AgdaAny -> AgdaAny -> AgdaAny
v6
= T_StrictTotalOrder_1036
-> (AgdaAny -> AgdaAny -> AgdaAny) -> [T_Tree_254] -> T_Tree_254
du_intersectionsWith_250 T_StrictTotalOrder_1036
v3 AgdaAny -> AgdaAny -> AgdaAny
v6
du_intersectionsWith_250 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_intersectionsWith_250 :: T_StrictTotalOrder_1036
-> (AgdaAny -> AgdaAny -> AgdaAny) -> [T_Tree_254] -> T_Tree_254
du_intersectionsWith_250 T_StrictTotalOrder_1036
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1036
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_254]
-> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_intersectionsWith_514 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny
v1))
d_intersections_254 ::
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.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
d_intersections_254 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> [T_Tree_254]
-> T_Tree_254
d_intersections_254 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5
= T_StrictTotalOrder_1036 -> [T_Tree_254] -> T_Tree_254
du_intersections_254 T_StrictTotalOrder_1036
v3
du_intersections_254 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_254] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_254
du_intersections_254 :: T_StrictTotalOrder_1036 -> [T_Tree_254] -> T_Tree_254
du_intersections_254 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> T_Value_38 -> [T_Tree_254] -> T_Tree_254)
-> AgdaAny -> AgdaAny -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe
T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
MAlonzo.Code.Data.Tree.AVL.du_intersections_524 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
(T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d__'8712''63'__256 ::
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 ->
() -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> Bool
d__'8712''63'__256 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> AgdaAny
-> T_Tree_254
-> Bool
d__'8712''63'__256 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> Bool
du__'8712''63'__256 T_StrictTotalOrder_1036
v3
du__'8712''63'__256 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_254 -> Bool
du__'8712''63'__256 :: T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> Bool
du__'8712''63'__256 T_StrictTotalOrder_1036
v0 = (T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> Bool)
-> AgdaAny -> AgdaAny -> T_Tree_254 -> Bool
forall a b. a -> b
coe T_StrictTotalOrder_1036 -> AgdaAny -> T_Tree_254 -> Bool
du_member_214 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)