{-# 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_44 :: p -> p -> p -> p -> p -> p -> ()
d_Tree_44 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Map_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_Map_206 :: () -> () -> () -> T_StrictTotalOrder_1280 -> () -> () -> ()
d_Map_206 = () -> () -> () -> T_StrictTotalOrder_1280 -> () -> () -> ()
forall a. a
erased
d_empty_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_empty_210 :: () -> () -> () -> T_StrictTotalOrder_1280 -> () -> () -> T_Tree_266
d_empty_210 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_Tree_266
du_empty_210
du_empty_210 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_empty_210 :: T_Tree_266
du_empty_210 = T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_empty_286
d_singleton_212 ::
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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_singleton_212 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> T_Tree_266
d_singleton_212 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = AgdaAny -> AgdaAny -> T_Tree_266
du_singleton_212
du_singleton_212 ::
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_singleton_212 :: AgdaAny -> AgdaAny -> T_Tree_266
du_singleton_212 = (AgdaAny -> AgdaAny -> T_Tree_266)
-> AgdaAny -> AgdaAny -> T_Tree_266
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_singleton_290
d_insert_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_insert_214 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
d_insert_214 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280
-> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_insert_214 T_StrictTotalOrder_1280
v3
du_insert_214 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_insert_214 :: T_StrictTotalOrder_1280
-> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_insert_214 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_insert_298 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_40)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.C_MkValue_52
(\ 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_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_insertWith_216 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
d_insertWith_216 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
du_insertWith_216 T_StrictTotalOrder_1280
v3
du_insertWith_216 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_insertWith_216 :: T_StrictTotalOrder_1280
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
du_insertWith_216 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_insertWith_308 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_40)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.C_MkValue_52
(\ 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_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_delete_218 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
d_delete_218 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_delete_218 T_StrictTotalOrder_1280
v3
du_delete_218 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_delete_218 :: T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_delete_218 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_delete_316 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
d_lookup_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> AgdaAny -> Maybe AgdaAny
d_lookup_220 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Tree_266
-> AgdaAny
-> Maybe AgdaAny
d_lookup_220 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
du_lookup_220 T_StrictTotalOrder_1280
v3
du_lookup_220 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> AgdaAny -> Maybe AgdaAny
du_lookup_220 :: T_StrictTotalOrder_1280 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
du_lookup_220 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Tree.AVL.du_lookup_324 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
d_map_222 ::
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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_map_222 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
d_map_222 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny
v8 = (AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
du_map_222 AgdaAny -> AgdaAny
v8
du_map_222 ::
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_map_222 :: (AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
du_map_222 AgdaAny -> AgdaAny
v0
= ((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266)
-> AgdaAny -> T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_map_346 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny -> AgdaAny
v0))
d_member_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> Bool
d_member_226 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> AgdaAny
-> T_Tree_266
-> Bool
d_member_226 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> Bool
du_member_226 T_StrictTotalOrder_1280
v3
du_member_226 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> Bool
du_member_226 :: T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> Bool
du_member_226 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> T_Tree_266 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_266 -> Bool
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> T_Tree_266 -> Bool
MAlonzo.Code.Data.Tree.AVL.du_member_362 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
d_headTail_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_228 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Tree_266
-> Maybe T_Σ_14
d_headTail_228 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_headTail_228 T_StrictTotalOrder_1280
v3
du_headTail_228 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_228 :: T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_headTail_228 T_StrictTotalOrder_1280
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> 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'__58 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_82)))
((T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
MAlonzo.Code.Data.Tree.AVL.du_headTail_368 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))
d_initLast_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_230 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Tree_266
-> Maybe T_Σ_14
d_initLast_230 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_initLast_230 T_StrictTotalOrder_1280
v3
du_initLast_230 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_230 :: T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_initLast_230 T_StrictTotalOrder_1280
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> 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'__58 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> T_K'38'__58 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_82))))
((T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
MAlonzo.Code.Data.Tree.AVL.du_initLast_380 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))
d_foldr_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_1280 ->
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_266 -> AgdaAny
d_foldr_232 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_266
-> AgdaAny
d_foldr_232 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny
du_foldr_232 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8
du_foldr_232 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> AgdaAny
du_foldr_232 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny
du_foldr_232 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.du_foldr_394 ((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_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_fromList_238 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> [T_Σ_14]
-> T_Tree_266
d_fromList_238 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> [T_Σ_14] -> T_Tree_266
du_fromList_238 T_StrictTotalOrder_1280
v3
du_fromList_238 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_fromList_238 :: T_StrictTotalOrder_1280 -> [T_Σ_14] -> T_Tree_266
du_fromList_238 T_StrictTotalOrder_1280
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_Σ_14] -> T_Tree_266
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
((T_StrictTotalOrder_1280
-> T_Value_40 -> [T_K'38'__58] -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40 -> [T_K'38'__58] -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_fromList_402 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96))
(((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'__58) -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__58
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_88))
d_toList_240 ::
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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
d_toList_240 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Tree_266
-> [T_Σ_14]
d_toList_240 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_Tree_266 -> [T_Σ_14]
du_toList_240
du_toList_240 ::
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
du_toList_240 :: T_Tree_266 -> [T_Σ_14]
du_toList_240
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> [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'__58 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_82))
((T_Tree_266 -> [T_K'38'__58]) -> AgdaAny
forall a b. a -> b
coe T_Tree_266 -> [T_K'38'__58]
MAlonzo.Code.Data.Tree.AVL.du_toList_404)
d_size_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> Integer
d_size_242 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Tree_266
-> Integer
d_size_242 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_Tree_266 -> Integer
du_size_242
du_size_242 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> Integer
du_size_242 :: T_Tree_266 -> Integer
du_size_242 = (T_Tree_266 -> Integer) -> T_Tree_266 -> Integer
forall a b. a -> b
coe T_Tree_266 -> Integer
MAlonzo.Code.Data.Tree.AVL.du_size_408
d_unionWith_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_1280 ->
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_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_unionWith_244 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_unionWith_244 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> Maybe AgdaAny -> AgdaAny
v8
= T_StrictTotalOrder_1280
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_unionWith_244 T_StrictTotalOrder_1280
v3 AgdaAny -> Maybe AgdaAny -> AgdaAny
v8
du_unionWith_244 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_unionWith_244 :: T_StrictTotalOrder_1280
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_unionWith_244 T_StrictTotalOrder_1280
v0 AgdaAny -> Maybe AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_unionWith_430 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v1))
d_union_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_union_248 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_union_248 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_union_248 T_StrictTotalOrder_1280
v3
du_union_248 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_union_248 :: T_StrictTotalOrder_1280 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_union_248 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_union_452 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
d_unionsWith_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_unionsWith_250 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
d_unionsWith_250 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 AgdaAny -> Maybe AgdaAny -> AgdaAny
v6
= T_StrictTotalOrder_1280
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
du_unionsWith_250 T_StrictTotalOrder_1280
v3 AgdaAny -> Maybe AgdaAny -> AgdaAny
v6
du_unionsWith_250 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_unionsWith_250 :: T_StrictTotalOrder_1280
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
du_unionsWith_250 T_StrictTotalOrder_1280
v0 AgdaAny -> Maybe AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_266] -> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_unionsWith_456 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v1))
d_unions_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_unions_254 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> [T_Tree_266]
-> T_Tree_266
d_unions_254 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> [T_Tree_266] -> T_Tree_266
du_unions_254 T_StrictTotalOrder_1280
v3
du_unions_254 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_unions_254 :: T_StrictTotalOrder_1280 -> [T_Tree_266] -> T_Tree_266
du_unions_254 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40 -> [T_Tree_266] -> T_Tree_266)
-> AgdaAny -> AgdaAny -> [T_Tree_266] -> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280 -> T_Value_40 -> [T_Tree_266] -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_unions_462 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
d_intersectionWith_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_1280 ->
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_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_intersectionWith_256 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_intersectionWith_256 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9 AgdaAny -> AgdaAny -> AgdaAny
v10
= T_StrictTotalOrder_1280
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_intersectionWith_256 T_StrictTotalOrder_1280
v3 AgdaAny -> AgdaAny -> AgdaAny
v10
du_intersectionWith_256 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_intersectionWith_256 :: T_StrictTotalOrder_1280
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_intersectionWith_256 T_StrictTotalOrder_1280
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1280
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_intersectionWith_488 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny
v1))
d_intersection_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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_intersection_260 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_intersection_260 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_intersection_260 T_StrictTotalOrder_1280
v3
du_intersection_260 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_intersection_260 :: T_StrictTotalOrder_1280 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_intersection_260 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_intersection_522 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
d_intersectionsWith_262 ::
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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_intersectionsWith_262 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
d_intersectionsWith_262 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 AgdaAny -> AgdaAny -> AgdaAny
v6
= T_StrictTotalOrder_1280
-> (AgdaAny -> AgdaAny -> AgdaAny) -> [T_Tree_266] -> T_Tree_266
du_intersectionsWith_262 T_StrictTotalOrder_1280
v3 AgdaAny -> AgdaAny -> AgdaAny
v6
du_intersectionsWith_262 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_intersectionsWith_262 :: T_StrictTotalOrder_1280
-> (AgdaAny -> AgdaAny -> AgdaAny) -> [T_Tree_266] -> T_Tree_266
du_intersectionsWith_262 T_StrictTotalOrder_1280
v0 AgdaAny -> AgdaAny -> AgdaAny
v1
= (T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_266] -> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_intersectionsWith_526 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny
v1))
d_intersections_266 ::
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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
d_intersections_266 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> [T_Tree_266]
-> T_Tree_266
d_intersections_266 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5
= T_StrictTotalOrder_1280 -> [T_Tree_266] -> T_Tree_266
du_intersections_266 T_StrictTotalOrder_1280
v3
du_intersections_266 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_266] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_266
du_intersections_266 :: T_StrictTotalOrder_1280 -> [T_Tree_266] -> T_Tree_266
du_intersections_266 T_StrictTotalOrder_1280
v0
= (T_StrictTotalOrder_1280
-> T_Value_40 -> [T_Tree_266] -> T_Tree_266)
-> AgdaAny -> AgdaAny -> [T_Tree_266] -> T_Tree_266
forall a b. a -> b
coe
T_StrictTotalOrder_1280 -> T_Value_40 -> [T_Tree_266] -> T_Tree_266
MAlonzo.Code.Data.Tree.AVL.du_intersections_536 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
(T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96)
d__'8712''63'__268 ::
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_1280 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> Bool
d__'8712''63'__268 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> AgdaAny
-> T_Tree_266
-> Bool
d__'8712''63'__268 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> Bool
du__'8712''63'__268 T_StrictTotalOrder_1280
v3
du__'8712''63'__268 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> Bool
du__'8712''63'__268 :: T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> Bool
du__'8712''63'__268 T_StrictTotalOrder_1280
v0 = (T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> Bool)
-> AgdaAny -> AgdaAny -> T_Tree_266 -> Bool
forall a b. a -> b
coe T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> Bool
du_member_226 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)