{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.Tree.AVL where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.DifferenceList
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Tree.AVL.Height
import qualified MAlonzo.Code.Data.Tree.AVL.Indexed
import qualified MAlonzo.Code.Data.Tree.AVL.Value
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict

-- Data.Tree.AVL.Indexed.K&_
d_K'38'__114 :: p -> p -> p -> p -> p -> p -> ()
d_K'38'__114 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed.Tree
d_Tree_122 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_Tree_122 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
-- Data.Tree.AVL.Indexed.Value
d_Value_124 :: p -> p -> p -> p -> p -> ()
d_Value_124 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Data.Tree.AVL.Indexed.const
d_const_132 ::
  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.Value.T_Value_40
d_const_132 :: () -> () -> () -> T_StrictTotalOrder_1280 -> () -> () -> T_Value_40
d_const_132 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 = () -> () -> T_Value_40
du_const_132
du_const_132 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40
du_const_132 :: () -> () -> T_Value_40
du_const_132 ()
v0 ()
v1
  = T_Value_40 -> T_Value_40
forall a b. a -> b
coe T_Value_40
MAlonzo.Code.Data.Tree.AVL.Value.du_const_96
-- Data.Tree.AVL.Indexed.fromPair
d_fromPair_140 ::
  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.Value.T_Value_40 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58
d_fromPair_140 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Σ_14
-> T_K'38'__58
d_fromPair_140 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 = () -> T_Value_40 -> T_Σ_14 -> T_K'38'__58
du_fromPair_140
du_fromPair_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58
du_fromPair_140 :: () -> T_Value_40 -> T_Σ_14 -> T_K'38'__58
du_fromPair_140 ()
v0 T_Value_40
v1 T_Σ_14
v2
  = (T_Σ_14 -> T_K'38'__58) -> T_Σ_14 -> T_K'38'__58
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__58
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_88 T_Σ_14
v2
-- Data.Tree.AVL.Indexed.toPair
d_toPair_194 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_194 :: T_K'38'__58 -> T_Σ_14
d_toPair_194 = (T_K'38'__58 -> T_Σ_14) -> T_K'38'__58 -> T_Σ_14
forall a b. a -> b
coe T_K'38'__58 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_82
-- Data.Tree.AVL.Indexed.K&_.key
d_key_216 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 -> AgdaAny
d_key_216 :: T_K'38'__58 -> AgdaAny
d_key_216 T_K'38'__58
v0
  = (T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v0)
-- Data.Tree.AVL.Indexed.K&_.value
d_value_218 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58 -> AgdaAny
d_value_218 :: T_K'38'__58 -> AgdaAny
d_value_218 T_K'38'__58
v0
  = (T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_70 (T_K'38'__58 -> AgdaAny
forall a b. a -> b
coe T_K'38'__58
v0)
-- Data.Tree.AVL.Indexed.Value.family
d_family_228 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_family_228 :: T_Value_40 -> AgdaAny -> ()
d_family_228 = T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL.Indexed.Value.respects
d_respects_230 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_230 :: T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_230 T_Value_40
v0
  = (T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_40 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_50 (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v0)
-- Data.Tree.AVL.Tree
d_Tree_266 :: p -> p -> p -> p -> p -> p -> ()
d_Tree_266 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Tree_266
  = C_tree_274 Integer MAlonzo.Code.Data.Tree.AVL.Indexed.T_Tree_192
-- Data.Tree.AVL._.Val
d_Val_284 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_284 :: T_Value_40 -> AgdaAny -> ()
d_Val_284 = T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.empty
d_empty_286 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> T_Tree_266
d_empty_286 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
d_empty_286 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 = T_Tree_266
du_empty_286
du_empty_286 :: T_Tree_266
du_empty_286 :: T_Tree_266
du_empty_286
  = let v0 :: t
v0 = (Integer -> T_Tree_192 -> T_Tree_266) -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_192 -> T_Tree_266
C_tree_274 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)) in
    AgdaAny -> T_Tree_266
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny
forall a. a
v0
         ((T__'60''8314'__20 -> T_Tree_192) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T__'60''8314'__20 -> T_Tree_192
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_204
            (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
               T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))
-- Data.Tree.AVL._.singleton
d_singleton_290 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> AgdaAny -> T_Tree_266
d_singleton_290 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_266
d_singleton_290 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 AgdaAny
v6 AgdaAny
v7
  = AgdaAny -> AgdaAny -> T_Tree_266
du_singleton_290 AgdaAny
v6 AgdaAny
v7
du_singleton_290 :: AgdaAny -> AgdaAny -> T_Tree_266
du_singleton_290 :: AgdaAny -> AgdaAny -> T_Tree_266
du_singleton_290 AgdaAny
v0 AgdaAny
v1
  = (Integer -> T_Tree_192 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> T_Tree_266
forall a b. a -> b
coe
      Integer -> T_Tree_192 -> T_Tree_266
C_tree_274 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer))
      ((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_192)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_192
MAlonzo.Code.Data.Tree.AVL.Indexed.du_singleton_810 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
            ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
               (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                  T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
            (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
               T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))
-- Data.Tree.AVL._.insert
d_insert_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
d_insert_298 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
d_insert_298 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 AgdaAny
v6 AgdaAny
v7 T_Tree_266
v8
  = T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_insert_298 T_StrictTotalOrder_1280
v3 T_Value_40
v5 AgdaAny
v6 AgdaAny
v7 T_Tree_266
v8
du_insert_298 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_insert_298 :: T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_insert_298 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_266
v4
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v4 of
      C_tree_274 Integer
v5 T_Tree_192
v6
        -> let v7 :: AgdaAny
v7
                 = (Integer -> T_Tree_192 -> T_Tree_266) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     Integer -> T_Tree_192 -> T_Tree_266
C_tree_274
                     ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                        ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> AgdaAny
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                              T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_932 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_192
v6
                              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                    (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                                       T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                                 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                                    T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))))
                        (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)) in
           AgdaAny -> T_Tree_266
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny
v7
                (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> AgdaAny
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_932 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_192
v6
                      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                            (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                               T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                         (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                            T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))))
      T_Tree_266
_ -> T_Tree_266
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.insertWith
d_insertWith_308 ::
  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.Value.T_Value_40 ->
  AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
d_insertWith_308 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
d_insertWith_308 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 AgdaAny
v6 Maybe AgdaAny -> AgdaAny
v7 T_Tree_266
v8
  = T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
du_insertWith_308 T_StrictTotalOrder_1280
v3 T_Value_40
v5 AgdaAny
v6 Maybe AgdaAny -> AgdaAny
v7 T_Tree_266
v8
du_insertWith_308 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
du_insertWith_308 :: T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
du_insertWith_308 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_266
v4
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v4 of
      C_tree_274 Integer
v5 T_Tree_192
v6
        -> let v7 :: AgdaAny
v7
                 = (Integer -> T_Tree_192 -> T_Tree_266) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     Integer -> T_Tree_192 -> T_Tree_266
C_tree_274
                     ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                        ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                              T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_830 (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
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v6)
                              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                    (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                                       T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                                 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                                    T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))))
                        (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)) in
           AgdaAny -> T_Tree_266
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny
v7
                (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_830 (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
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v6)
                      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                            (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                               T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                         (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                            T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))))
      T_Tree_266
_ -> T_Tree_266
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.delete
d_delete_316 ::
  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.Value.T_Value_40 ->
  AgdaAny -> T_Tree_266 -> T_Tree_266
d_delete_316 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
d_delete_316 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 AgdaAny
v6 T_Tree_266
v7 = T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_delete_316 T_StrictTotalOrder_1280
v3 AgdaAny
v6 T_Tree_266
v7
du_delete_316 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  AgdaAny -> T_Tree_266 -> T_Tree_266
du_delete_316 :: T_StrictTotalOrder_1280 -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_delete_316 T_StrictTotalOrder_1280
v0 AgdaAny
v1 T_Tree_266
v2
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v2 of
      C_tree_274 Integer
v3 T_Tree_192
v4
        -> let v5 :: AgdaAny
v5
                 = (Integer -> T_Tree_192 -> T_Tree_266) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     Integer -> T_Tree_192 -> T_Tree_266
C_tree_274
                     ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                        ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                              T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_948 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
                              ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                              (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)
                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v4)
                              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                    (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                                       T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                                 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                                    T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))))
                        (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)) in
           AgdaAny -> T_Tree_266
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny
v5
                (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_192
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_192
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_948 (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
                      ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                         (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                      (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)
                      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v4)
                      ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                            (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                               T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                         (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                            T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))))
      T_Tree_266
_ -> T_Tree_266
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.lookup
d_lookup_324 ::
  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.Value.T_Value_40 ->
  T_Tree_266 -> AgdaAny -> Maybe AgdaAny
d_lookup_324 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
-> AgdaAny
-> Maybe AgdaAny
d_lookup_324 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 T_Tree_266
v6 AgdaAny
v7
  = T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
du_lookup_324 T_StrictTotalOrder_1280
v3 T_Value_40
v5 T_Tree_266
v6 AgdaAny
v7
du_lookup_324 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  T_Tree_266 -> AgdaAny -> Maybe AgdaAny
du_lookup_324 :: T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
du_lookup_324 T_StrictTotalOrder_1280
v0 T_Value_40
v1 T_Tree_266
v2 AgdaAny
v3
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v2 of
      C_tree_274 Integer
v4 T_Tree_192
v5
        -> (T_StrictTotalOrder_1280
 -> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
             T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_192 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
MAlonzo.Code.Data.Tree.AVL.Indexed.du_lookup_1046 (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
v1)
             (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
             ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                   (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                      T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                   T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30))
      T_Tree_266
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_342 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_342 :: T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
d_Val_342 = T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_344 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Wal_344 :: T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
d_Wal_344 = T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.map
d_map_346 ::
  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.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
d_map_346 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
d_map_346 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~T_Value_40
v6 ~T_Value_40
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_266
v9 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
du_map_346 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_266
v9
du_map_346 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
du_map_346 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_266 -> T_Tree_266
du_map_346 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_266
v1
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v1 of
      C_tree_274 Integer
v2 T_Tree_192
v3
        -> (Integer -> T_Tree_192 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> T_Tree_266
forall a b. a -> b
coe
             Integer -> T_Tree_192 -> T_Tree_266
C_tree_274 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
             (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_192 -> T_Tree_192
MAlonzo.Code.Data.Tree.AVL.Indexed.du_map_1200 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v3))
      T_Tree_266
_ -> T_Tree_266
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_360 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_360 :: T_Value_40 -> AgdaAny -> ()
d_Val_360 = T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.member
d_member_362 ::
  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.Value.T_Value_40 ->
  AgdaAny -> T_Tree_266 -> Bool
d_member_362 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> AgdaAny
-> T_Tree_266
-> Bool
d_member_362 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 AgdaAny
v6 T_Tree_266
v7
  = T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> T_Tree_266 -> Bool
du_member_362 T_StrictTotalOrder_1280
v3 T_Value_40
v5 AgdaAny
v6 T_Tree_266
v7
du_member_362 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> T_Tree_266 -> Bool
du_member_362 :: T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> T_Tree_266 -> Bool
du_member_362 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny
v2 T_Tree_266
v3
  = (Maybe AgdaAny -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
      Maybe AgdaAny -> Bool
MAlonzo.Code.Data.Maybe.Base.du_is'45'just_20
      ((T_StrictTotalOrder_1280
 -> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
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
v1) (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.Tree.AVL._.headTail
d_headTail_368 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  T_Tree_266 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_368 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
-> Maybe T_Σ_14
d_headTail_368 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 T_Tree_266
v6 = T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_headTail_368 T_StrictTotalOrder_1280
v3 T_Tree_266
v6
du_headTail_368 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  T_Tree_266 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_368 :: T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_headTail_368 T_StrictTotalOrder_1280
v0 T_Tree_266
v1
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v1 of
      C_tree_274 Integer
v2 T_Tree_192
v3
        -> let v4 :: AgdaAny
v4
                 = let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (let v5 :: AgdaAny
v5
                            = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                Integer -> T_Tree_192 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_headTail_660 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
                                (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v3) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v5 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v7 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
                                    -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v9 of
                                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
                                           -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                                                   ((Integer -> T_Tree_192 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                      Integer -> T_Tree_192 -> T_Tree_266
C_tree_274
                                                      ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
                                                      ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T_Tree_192
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_192
-> T_Tree_192
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'737'_302
                                                         (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
                                                         ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                               Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                                                         ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                               AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                               ((T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                  T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68
                                                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
                                                         (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                                                         ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                                            (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
                                                               T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11))))
                                         T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v3 of
                MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_204 T__'60''8314'__20
v5
                  -> Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                T_Tree_192
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
      T_Tree_266
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.initLast
d_initLast_380 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  T_Tree_266 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_380 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
-> Maybe T_Σ_14
d_initLast_380 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 T_Tree_266
v6 = T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_initLast_380 T_StrictTotalOrder_1280
v3 T_Tree_266
v6
du_initLast_380 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  T_Tree_266 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_380 :: T_StrictTotalOrder_1280 -> T_Tree_266 -> Maybe T_Σ_14
du_initLast_380 T_StrictTotalOrder_1280
v0 T_Tree_266
v1
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v1 of
      C_tree_274 Integer
v2 T_Tree_192
v3
        -> let v4 :: AgdaAny
v4
                 = let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     (let v5 :: AgdaAny
v5
                            = (Integer -> T_Tree_192 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                Integer -> T_Tree_192 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_initLast_710 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
                                (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v3) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v5 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v7 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
                                    -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v9 of
                                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
                                           -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   ((Integer -> T_Tree_192 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                      Integer -> T_Tree_192 -> T_Tree_266
C_tree_274
                                                      ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
                                                      ((T_StrictTotalOrder_1280
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_192
 -> T__'60''8314'__20
 -> T_Tree_192)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_192
-> T__'60''8314'__20
-> T_Tree_192
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'691'_328
                                                         (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)
                                                         ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                               Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                                                         ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                               AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                               ((T_K'38'__58 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                  T_K'38'__58 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_68
                                                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
                                                         (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                                                         (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
                                                            T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)))
                                                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
                                         T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_192 -> T_Tree_192
forall a b. a -> b
coe T_Tree_192
v3 of
                MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_204 T__'60''8314'__20
v5
                  -> Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                T_Tree_192
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
      T_Tree_266
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.foldr
d_foldr_394 ::
  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.Value.T_Value_40 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_266 -> AgdaAny
d_foldr_394 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_266
-> AgdaAny
d_foldr_394 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 T_Tree_266
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny
du_foldr_394 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 T_Tree_266
v10
du_foldr_394 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_266 -> AgdaAny
du_foldr_394 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny
du_foldr_394 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_266
v2
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v2 of
      C_tree_274 Integer
v3 T_Tree_192
v4
        -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_192 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_192 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Indexed.du_foldr_1126 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
             (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v4)
      T_Tree_266
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.fromList
d_fromList_402 ::
  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.Value.T_Value_40 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58] -> T_Tree_266
d_fromList_402 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> [T_K'38'__58]
-> T_Tree_266
d_fromList_402 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 = T_StrictTotalOrder_1280
-> T_Value_40 -> [T_K'38'__58] -> T_Tree_266
du_fromList_402 T_StrictTotalOrder_1280
v3 T_Value_40
v5
du_fromList_402 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58] -> T_Tree_266
du_fromList_402 :: T_StrictTotalOrder_1280
-> T_Value_40 -> [T_K'38'__58] -> T_Tree_266
du_fromList_402 T_StrictTotalOrder_1280
v0 T_Value_40
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_K'38'__58] -> T_Tree_266
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
         (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244
            ((T_StrictTotalOrder_1280
 -> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_insert_298 (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
v1)))
         ((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 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
du_empty_286)
-- Data.Tree.AVL._.toList
d_toList_404 ::
  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.Value.T_Value_40 ->
  T_Tree_266 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58]
d_toList_404 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
-> [T_K'38'__58]
d_toList_404 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 T_Tree_266
v6 = T_Tree_266 -> [T_K'38'__58]
du_toList_404 T_Tree_266
v6
du_toList_404 ::
  T_Tree_266 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__58]
du_toList_404 :: T_Tree_266 -> [T_K'38'__58]
du_toList_404 T_Tree_266
v0
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v0 of
      C_tree_274 Integer
v1 T_Tree_192
v2
        -> (([AgdaAny] -> [AgdaAny]) -> [AgdaAny]) -> AgdaAny -> [T_K'38'__58]
forall a b. a -> b
coe
             ([AgdaAny] -> [AgdaAny]) -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du_toList_54
             ((T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Tree_192 -> [T_K'38'__58] -> [T_K'38'__58]
MAlonzo.Code.Data.Tree.AVL.Indexed.du_toDiffList_1152 (T_Tree_192 -> AgdaAny
forall a b. a -> b
coe T_Tree_192
v2))
      T_Tree_266
_ -> [T_K'38'__58]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.size
d_size_408 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  T_Tree_266 -> Integer
d_size_408 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
-> Integer
d_size_408 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1280
v3 ~()
v4 ~T_Value_40
v5 T_Tree_266
v6 = T_Tree_266 -> Integer
du_size_408 T_Tree_266
v6
du_size_408 :: T_Tree_266 -> Integer
du_size_408 :: T_Tree_266 -> Integer
du_size_408 T_Tree_266
v0
  = case T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
v0 of
      C_tree_274 Integer
v1 T_Tree_192
v2
        -> (T_Tree_192 -> Integer) -> T_Tree_192 -> Integer
forall a b. a -> b
coe T_Tree_192 -> Integer
MAlonzo.Code.Data.Tree.AVL.Indexed.du_size_1176 T_Tree_192
v2
      T_Tree_266
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_424 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_424 :: T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
d_Val_424 = T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_426 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Wal_426 :: T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
d_Wal_426 = T_StrictTotalOrder_1280
-> () -> () -> T_Value_40 -> T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.unionWith
d_unionWith_430 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
d_unionWith_430 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_unionWith_430 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~T_Value_40
v6 T_Value_40
v7 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v8 T_Tree_266
v9 T_Tree_266
v10
  = T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_unionWith_430 T_StrictTotalOrder_1280
v3 T_Value_40
v7 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v8 T_Tree_266
v9 T_Tree_266
v10
du_unionWith_430 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_unionWith_430 :: T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_unionWith_430 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 T_Tree_266
v3 T_Tree_266
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_266 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_266
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny
du_foldr_394
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v5 AgdaAny
v6 ->
            (T_StrictTotalOrder_1280
 -> T_Value_40
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_266
 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
-> T_Value_40
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
du_insertWith_308 (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
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)))
      (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
v4) (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
v3)
-- Data.Tree.AVL._.Val
d_Val_450 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_450 :: T_Value_40 -> AgdaAny -> ()
d_Val_450 = T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.union
d_union_452 ::
  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.Value.T_Value_40 ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
d_union_452 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_union_452 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 = T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_union_452 T_StrictTotalOrder_1280
v3 T_Value_40
v5
du_union_452 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_union_452 :: T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_union_452 T_StrictTotalOrder_1280
v0 T_Value_40
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
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
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL._.unionsWith
d_unionsWith_456 ::
  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.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  [T_Tree_266] -> T_Tree_266
d_unionsWith_456 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
d_unionsWith_456 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v6 [T_Tree_266]
v7
  = T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
du_unionsWith_456 T_StrictTotalOrder_1280
v3 T_Value_40
v5 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v6 [T_Tree_266]
v7
du_unionsWith_456 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  [T_Tree_266] -> T_Tree_266
du_unionsWith_456 :: T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
du_unionsWith_456 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 [T_Tree_266]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_266
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
 -> T_Tree_266
 -> T_Tree_266
 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
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
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
v1) ((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2))
      (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
du_empty_286) ([T_Tree_266] -> AgdaAny
forall a b. a -> b
coe [T_Tree_266]
v3)
-- Data.Tree.AVL._.unions
d_unions_462 ::
  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.Value.T_Value_40 ->
  [T_Tree_266] -> T_Tree_266
d_unions_462 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> [T_Tree_266]
-> T_Tree_266
d_unions_462 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 = T_StrictTotalOrder_1280 -> T_Value_40 -> [T_Tree_266] -> T_Tree_266
du_unions_462 T_StrictTotalOrder_1280
v3 T_Value_40
v5
du_unions_462 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  [T_Tree_266] -> T_Tree_266
du_unions_462 :: T_StrictTotalOrder_1280 -> T_Value_40 -> [T_Tree_266] -> T_Tree_266
du_unions_462 T_StrictTotalOrder_1280
v0 T_Value_40
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
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
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL._.Val
d_Val_480 ::
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_480 :: T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> ()
d_Val_480 = T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_482 ::
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Wal_482 :: T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> ()
d_Wal_482 = T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> ()
forall a. a
erased
-- Data.Tree.AVL._.Xal
d_Xal_484 ::
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Xal_484 :: T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> ()
d_Xal_484 = T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> AgdaAny
-> ()
forall a. a
erased
-- Data.Tree.AVL._.intersectionWith
d_intersectionWith_488 ::
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
d_intersectionWith_488 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_intersectionWith_488 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_40
v7 T_Value_40
v8 T_Value_40
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_266
v11
                       T_Tree_266
v12
  = T_StrictTotalOrder_1280
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_intersectionWith_488 T_StrictTotalOrder_1280
v3 T_Value_40
v8 T_Value_40
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_266
v11 T_Tree_266
v12
du_intersectionWith_488 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_intersectionWith_488 :: T_StrictTotalOrder_1280
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
du_intersectionWith_488 T_StrictTotalOrder_1280
v0 T_Value_40
v1 T_Value_40
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Tree_266
v4 T_Tree_266
v5
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_266 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_266
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_266 -> AgdaAny
du_foldr_394
      ((T_StrictTotalOrder_1280
 -> T_Value_40
 -> T_Value_40
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Tree_266
 -> AgdaAny
 -> AgdaAny
 -> T_Tree_266
 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
du_cons_502 (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
v1) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
v5))
      (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
du_empty_286) (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
v4)
-- Data.Tree.AVL._._.cons
d_cons_502 ::
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_266 ->
  T_Tree_266 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
d_cons_502 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> ()
-> ()
-> T_Value_40
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> T_Tree_266
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
d_cons_502 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_40
v7 T_Value_40
v8 T_Value_40
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Tree_266
v11 T_Tree_266
v12 AgdaAny
v13
           AgdaAny
v14
  = T_StrictTotalOrder_1280
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
du_cons_502 T_StrictTotalOrder_1280
v3 T_Value_40
v8 T_Value_40
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_266
v12 AgdaAny
v13 AgdaAny
v14
du_cons_502 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_266 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_cons_502 :: T_StrictTotalOrder_1280
-> T_Value_40
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_266
-> AgdaAny
-> AgdaAny
-> T_Tree_266
-> T_Tree_266
du_cons_502 T_StrictTotalOrder_1280
v0 T_Value_40
v1 T_Value_40
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Tree_266
v4 AgdaAny
v5 AgdaAny
v6
  = let v7 :: AgdaAny
v7 = (T_StrictTotalOrder_1280
 -> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> AgdaAny -> Maybe AgdaAny
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
v1) (T_Tree_266 -> AgdaAny
forall a b. a -> b
coe T_Tree_266
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) in
    AgdaAny -> T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe
      (case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
v7 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v8
           -> (T_StrictTotalOrder_1280
 -> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> AgdaAny -> T_Tree_266 -> T_Tree_266
du_insert_298 (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
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
         Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v8 -> AgdaAny
v8)
         Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL._.Val
d_Val_520 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 -> AgdaAny -> ()
d_Val_520 :: T_Value_40 -> AgdaAny -> ()
d_Val_520 = T_Value_40 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.intersection
d_intersection_522 ::
  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.Value.T_Value_40 ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
d_intersection_522 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> T_Tree_266
-> T_Tree_266
-> T_Tree_266
d_intersection_522 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5
  = T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_intersection_522 T_StrictTotalOrder_1280
v3 T_Value_40
v5
du_intersection_522 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_intersection_522 :: T_StrictTotalOrder_1280
-> T_Value_40 -> T_Tree_266 -> T_Tree_266 -> T_Tree_266
du_intersection_522 T_StrictTotalOrder_1280
v0 T_Value_40
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
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
v1) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL._.intersectionsWith
d_intersectionsWith_526 ::
  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.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [T_Tree_266] -> T_Tree_266
d_intersectionsWith_526 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
d_intersectionsWith_526 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [T_Tree_266]
v7
  = T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
du_intersectionsWith_526 T_StrictTotalOrder_1280
v3 T_Value_40
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [T_Tree_266]
v7
du_intersectionsWith_526 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [T_Tree_266] -> T_Tree_266
du_intersectionsWith_526 :: T_StrictTotalOrder_1280
-> T_Value_40
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_266]
-> T_Tree_266
du_intersectionsWith_526 T_StrictTotalOrder_1280
v0 T_Value_40
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 [T_Tree_266]
v3
  = case [T_Tree_266] -> [AgdaAny]
forall a b. a -> b
coe [T_Tree_266]
v3 of
      [] -> T_Tree_266 -> T_Tree_266
forall a b. a -> b
coe T_Tree_266
du_empty_286
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_266
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldl_230
             ((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 -> AgdaAny
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
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
v1) (T_Value_40 -> AgdaAny
forall a b. a -> b
coe T_Value_40
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2))
             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5)
      [AgdaAny]
_ -> T_Tree_266
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.intersections
d_intersections_536 ::
  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.Value.T_Value_40 ->
  [T_Tree_266] -> T_Tree_266
d_intersections_536 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> [T_Tree_266]
-> T_Tree_266
d_intersections_536 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5
  = T_StrictTotalOrder_1280 -> T_Value_40 -> [T_Tree_266] -> T_Tree_266
du_intersections_536 T_StrictTotalOrder_1280
v3 T_Value_40
v5
du_intersections_536 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  [T_Tree_266] -> T_Tree_266
du_intersections_536 :: T_StrictTotalOrder_1280 -> T_Value_40 -> [T_Tree_266] -> T_Tree_266
du_intersections_536 T_StrictTotalOrder_1280
v0 T_Value_40
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
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
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL._∈?_
d__'8712''63'__542 ::
  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.Value.T_Value_40 ->
  AgdaAny -> T_Tree_266 -> Bool
d__'8712''63'__542 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1280
-> ()
-> T_Value_40
-> AgdaAny
-> T_Tree_266
-> Bool
d__'8712''63'__542 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1280
v3 ~()
v4 T_Value_40
v5
  = T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> T_Tree_266 -> Bool
du__'8712''63'__542 T_StrictTotalOrder_1280
v3 T_Value_40
v5
du__'8712''63'__542 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_40 ->
  AgdaAny -> T_Tree_266 -> Bool
du__'8712''63'__542 :: T_StrictTotalOrder_1280
-> T_Value_40 -> AgdaAny -> T_Tree_266 -> Bool
du__'8712''63'__542 T_StrictTotalOrder_1280
v0 T_Value_40
v1 = (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
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
v1)