{-# 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
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_178 ::
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 -> () -> ()
d_Map_178 :: () -> () -> () -> T_StrictTotalOrder_864 -> () -> () -> ()
d_Map_178 = () -> () -> () -> T_StrictTotalOrder_864 -> () -> () -> ()
forall a. a
erased
d_empty_182 ::
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.T_Tree_240
d_empty_182 :: () -> () -> () -> T_StrictTotalOrder_864 -> () -> () -> T_Tree_240
d_empty_182 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_Tree_240
du_empty_182
du_empty_182 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_empty_182 :: T_Tree_240
du_empty_182 = T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_empty_260
d_singleton_184 ::
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 ->
() -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_singleton_184 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> T_Tree_240
d_singleton_184 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_184
du_singleton_184 ::
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_singleton_184 :: AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_184 = (AgdaAny -> AgdaAny -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_singleton_264
d_insert_186 ::
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 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_insert_186 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_insert_186 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864
-> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_186 T_StrictTotalOrder_864
v3
du_insert_186 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_insert_186 :: T_StrictTotalOrder_864
-> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_186 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_insert_272 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_188 ::
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 ->
() ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_insertWith_188 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
d_insertWith_188 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_188 T_StrictTotalOrder_864
v3
du_insertWith_188 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_insertWith_188 :: T_StrictTotalOrder_864
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_188 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_insertWith_282 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_190 ::
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 ->
() ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_delete_190 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_delete_190 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_190 T_StrictTotalOrder_864
v3
du_delete_190 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
AgdaAny ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_delete_190 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_190 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_delete_290 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
d_lookup_192 ::
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 ->
() ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> Maybe AgdaAny
d_lookup_192 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> AgdaAny
-> T_Tree_240
-> Maybe AgdaAny
d_lookup_192 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_192 T_StrictTotalOrder_864
v3
du_lookup_192 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> Maybe AgdaAny
du_lookup_192 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_192 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
MAlonzo.Code.Data.Tree.AVL.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
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_map_194 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
d_map_194 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny
v8 = (AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_194 AgdaAny -> AgdaAny
v8
du_map_194 ::
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_map_194 :: (AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_194 AgdaAny -> AgdaAny
v0
= ((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_map_320 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny -> AgdaAny
v0))
d__'8712''63'__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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> Bool
d__'8712''63'__198 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> AgdaAny
-> T_Tree_240
-> Bool
d__'8712''63'__198 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__198 T_StrictTotalOrder_864
v3
du__'8712''63'__198 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> Bool
du__'8712''63'__198 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__198 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240 -> Bool
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Bool
MAlonzo.Code.Data.Tree.AVL.du__'8712''63'__336 (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
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_headTail_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_200 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Tree_240
-> Maybe T_Σ_14
d_headTail_200 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_headTail_200 T_StrictTotalOrder_864
v3
du_headTail_200 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_200 :: T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_headTail_200 T_StrictTotalOrder_864
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_240 -> Maybe T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
(((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_68
(((AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map'8321'_158
((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_864 -> T_Tree_240 -> Maybe T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
MAlonzo.Code.Data.Tree.AVL.du_headTail_342 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
d_initLast_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_202 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Tree_240
-> Maybe T_Σ_14
d_initLast_202 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_initLast_202 T_StrictTotalOrder_864
v3
du_initLast_202 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_202 :: T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_initLast_202 T_StrictTotalOrder_864
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_240 -> Maybe T_Σ_14
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
(((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_68
(((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.du_map'8322'_170
((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_864 -> T_Tree_240 -> Maybe T_Σ_14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
MAlonzo.Code.Data.Tree.AVL.du_initLast_356 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
d_foldr_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_864 ->
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_240 -> AgdaAny
d_foldr_204 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_240
-> AgdaAny
d_foldr_204 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_204 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8
du_foldr_204 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> AgdaAny
du_foldr_204 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_204 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
= ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_240 -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.du_foldr_372 ((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_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_fromList_210 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> [T_Σ_14]
-> T_Tree_240
d_fromList_210 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> [T_Σ_14] -> T_Tree_240
du_fromList_210 T_StrictTotalOrder_864
v3
du_fromList_210 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_fromList_210 :: T_StrictTotalOrder_864 -> [T_Σ_14] -> T_Tree_240
du_fromList_210 T_StrictTotalOrder_864
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_Σ_14] -> T_Tree_240
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
((T_StrictTotalOrder_864
-> T_Value_38 -> [T_K'38'__56] -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864 -> T_Value_38 -> [T_K'38'__56] -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_fromList_380 (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
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_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
d_toList_212 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Tree_240
-> [T_Σ_14]
d_toList_212 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_Tree_240 -> [T_Σ_14]
du_toList_212
du_toList_212 ::
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
[MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14]
du_toList_212 :: T_Tree_240 -> [T_Σ_14]
du_toList_212
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_240 -> [T_Σ_14]
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
(((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_240 -> [T_K'38'__56]) -> AgdaAny
forall a b. a -> b
coe T_Tree_240 -> [T_K'38'__56]
MAlonzo.Code.Data.Tree.AVL.du_toList_382)
d_size_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> Integer
d_size_214 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Tree_240
-> Integer
d_size_214 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_Tree_240 -> Integer
du_size_214
du_size_214 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_240 -> Integer
du_size_214 :: T_Tree_240 -> Integer
du_size_214 = (T_Tree_240 -> Integer) -> T_Tree_240 -> Integer
forall a b. a -> b
coe T_Tree_240 -> Integer
MAlonzo.Code.Data.Tree.AVL.du_size_386
d_unionWith_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_864 ->
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_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_unionWith_216 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_unionWith_216 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 AgdaAny -> Maybe AgdaAny -> AgdaAny
v8
= T_StrictTotalOrder_864
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_216 T_StrictTotalOrder_864
v3 AgdaAny -> Maybe AgdaAny -> AgdaAny
v8
du_unionWith_216 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_unionWith_216 :: T_StrictTotalOrder_864
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_216 T_StrictTotalOrder_864
v0 AgdaAny -> Maybe AgdaAny -> AgdaAny
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
MAlonzo.Code.Data.Tree.AVL.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
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_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_union_220 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_union_220 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_220 T_StrictTotalOrder_864
v3
du_union_220 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_union_220 :: T_StrictTotalOrder_864 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_220 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_union_430 (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
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_unionsWith_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_unionsWith_222 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
d_unionsWith_222 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 AgdaAny -> Maybe AgdaAny -> AgdaAny
v6
= T_StrictTotalOrder_864
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_222 T_StrictTotalOrder_864
v3 AgdaAny -> Maybe AgdaAny -> AgdaAny
v6
du_unionsWith_222 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
(AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_unionsWith_222 :: T_StrictTotalOrder_864
-> (AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_222 T_StrictTotalOrder_864
v0 AgdaAny -> Maybe AgdaAny -> AgdaAny
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
MAlonzo.Code.Data.Tree.AVL.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
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_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_unions_226 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> [T_Tree_240]
-> T_Tree_240
d_unions_226 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> [T_Tree_240] -> T_Tree_240
du_unions_226 T_StrictTotalOrder_864
v3
du_unions_226 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_unions_226 :: T_StrictTotalOrder_864 -> [T_Tree_240] -> T_Tree_240
du_unions_226 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38 -> [T_Tree_240] -> T_Tree_240)
-> AgdaAny -> AgdaAny -> [T_Tree_240] -> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_unions_440 (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
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_intersectionWith_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_864 ->
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_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_intersectionWith_228 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_intersectionWith_228 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~()
v7 ~()
v8 ~()
v9 AgdaAny -> AgdaAny -> AgdaAny
v10
= T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_228 T_StrictTotalOrder_864
v3 AgdaAny -> AgdaAny -> AgdaAny
v10
du_intersectionWith_228 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_intersectionWith_228 :: T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_228 T_StrictTotalOrder_864
v0 AgdaAny -> AgdaAny -> AgdaAny
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
MAlonzo.Code.Data.Tree.AVL.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
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_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_intersection_232 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_intersection_232 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 = T_StrictTotalOrder_864 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_232 T_StrictTotalOrder_864
v3
du_intersection_232 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240 ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_intersection_232 :: T_StrictTotalOrder_864 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_232 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_intersection_500 (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
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)
d_intersectionsWith_234 ::
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 ->
() ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_intersectionsWith_234 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
d_intersectionsWith_234 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 AgdaAny -> AgdaAny -> AgdaAny
v6
= T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny -> AgdaAny) -> [T_Tree_240] -> T_Tree_240
du_intersectionsWith_234 T_StrictTotalOrder_864
v3 AgdaAny -> AgdaAny -> AgdaAny
v6
du_intersectionsWith_234 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_intersectionsWith_234 :: T_StrictTotalOrder_864
-> (AgdaAny -> AgdaAny -> AgdaAny) -> [T_Tree_240] -> T_Tree_240
du_intersectionsWith_234 T_StrictTotalOrder_864
v0 AgdaAny -> AgdaAny -> AgdaAny
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
MAlonzo.Code.Data.Tree.AVL.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
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_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_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
d_intersections_238 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> [T_Tree_240]
-> T_Tree_240
d_intersections_238 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5
= T_StrictTotalOrder_864 -> [T_Tree_240] -> T_Tree_240
du_intersections_238 T_StrictTotalOrder_864
v3
du_intersections_238 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
[MAlonzo.Code.Data.Tree.AVL.T_Tree_240] ->
MAlonzo.Code.Data.Tree.AVL.T_Tree_240
du_intersections_238 :: T_StrictTotalOrder_864 -> [T_Tree_240] -> T_Tree_240
du_intersections_238 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> T_Value_38 -> [T_Tree_240] -> T_Tree_240)
-> AgdaAny -> AgdaAny -> [T_Tree_240] -> T_Tree_240
forall a b. a -> b
coe
T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
MAlonzo.Code.Data.Tree.AVL.du_intersections_514 (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
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94)