{-# 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'__106 :: p -> p -> p -> p -> p -> p -> ()
d_K'38'__106 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed.Tree
d_Tree_112 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_Tree_112 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_114 :: p -> p -> p -> p -> p -> ()
d_Value_114 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Data.Tree.AVL.Indexed.const
d_const_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
d_const_120 :: () -> () -> () -> T_StrictTotalOrder_1036 -> () -> () -> T_Value_38
d_const_120 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 = () -> () -> T_Value_38
du_const_120
du_const_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_120 :: () -> () -> T_Value_38
du_const_120 ()
v0 ()
v1
  = T_Value_38 -> T_Value_38
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94
-- Data.Tree.AVL.Indexed.fromPair
d_fromPair_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
d_fromPair_128 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_128 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 = () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_128
du_fromPair_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
du_fromPair_128 :: () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_128 ()
v0 T_Value_38
v1 T_Σ_14
v2
  = (T_Σ_14 -> T_K'38'__56) -> T_Σ_14 -> T_K'38'__56
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_86 T_Σ_14
v2
-- Data.Tree.AVL.Indexed.toPair
d_toPair_182 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_182 :: T_K'38'__56 -> T_Σ_14
d_toPair_182 T_K'38'__56
v0
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0))
      ((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0))
-- Data.Tree.AVL.Indexed.K&_.key
d_key_204 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_204 :: T_K'38'__56 -> Any
d_key_204 T_K'38'__56
v0
  = (T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed.K&_.value
d_value_206 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_206 :: T_K'38'__56 -> Any
d_value_206 T_K'38'__56
v0
  = (T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> Any
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed.Value.family
d_family_216 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_216 :: T_Value_38 -> Any -> ()
d_family_216 = T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL.Indexed.Value.respects
d_respects_218 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_218 :: T_Value_38 -> Any -> Any -> Any -> Any -> Any
d_respects_218 T_Value_38
v0
  = (T_Value_38 -> Any -> Any -> Any -> Any -> Any)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Value_38 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v0)
-- Data.Tree.AVL.Tree
d_Tree_254 :: p -> p -> p -> p -> p -> p -> ()
d_Tree_254 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Tree_254
  = C_tree_262 Integer MAlonzo.Code.Data.Tree.AVL.Indexed.T_Tree_180
-- Data.Tree.AVL._.Val
d_Val_272 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_272 :: T_Value_38 -> Any -> ()
d_Val_272 = T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.empty
d_empty_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> T_Tree_254
d_empty_274 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
d_empty_274 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 = T_Tree_254
du_empty_274
du_empty_274 :: T_Tree_254
du_empty_274 :: T_Tree_254
du_empty_274
  = let v0 :: t
v0 = (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Tree_254
C_tree_262 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) in
    Any -> T_Tree_254
forall a b. a -> b
coe
      (Any -> Any -> Any
forall a b. a -> b
coe
         Any
forall a. a
v0
         ((T__'60''8314'__20 -> T_Tree_180) -> Any -> Any
forall a b. a -> b
coe
            T__'60''8314'__20 -> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_192
            (T__'60''8314'__20 -> Any
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_278 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> T_Tree_254
d_singleton_278 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> Any
-> T_Tree_254
d_singleton_278 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 Any
v6 Any
v7
  = Any -> Any -> T_Tree_254
du_singleton_278 Any
v6 Any
v7
du_singleton_278 :: AgdaAny -> AgdaAny -> T_Tree_254
du_singleton_278 :: Any -> Any -> T_Tree_254
du_singleton_278 Any
v0 Any
v1
  = (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
      Integer -> T_Tree_180 -> T_Tree_254
C_tree_262 (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
      ((Any -> Any -> T_Σ_14 -> T_Tree_180) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Σ_14 -> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_singleton_798 (Any -> Any
forall a b. a -> b
coe Any
v0)
         (Any -> Any
forall a b. a -> b
coe Any
v1)
         ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
            Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
            ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
               Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
               (T__'60''8331'__20 -> Any
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 -> Any
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_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_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
d_insert_286 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
d_insert_286 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any
v6 Any
v7 T_Tree_254
v8
  = T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any
v6 Any
v7 T_Tree_254
v8
du_insert_286 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_insert_286 :: T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Any
v3 T_Tree_254
v4
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v4 of
      C_tree_262 Integer
v5 T_Tree_180
v6
        -> let v7 :: t
v7
                 = (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe
                     Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
                     ((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                        ((T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
                           T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_1036
 -> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14)
-> T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> Any
-> T_Tree_180
-> Any
-> Any
forall a b. a -> b
coe
                              T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_920 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Any
v3 T_Tree_180
v6
                              ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                 Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                                    Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                    (T__'60''8331'__20 -> Any
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 -> Any
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 -> Any
forall a b. a -> b
coe Integer
v5)) in
           Any -> T_Tree_254
forall a b. a -> b
coe
             (Any -> Any -> Any
forall a b. a -> b
coe
                Any
forall a. a
v7
                (T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_1036
 -> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14)
-> T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> Any
-> T_Tree_180
-> Any
-> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_180 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_920 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Any
v3 T_Tree_180
v6
                      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                            Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                            (T__'60''8331'__20 -> Any
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 -> Any
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_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.insertWith
d_insertWith_296 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
d_insertWith_296 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
d_insertWith_296 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any
v6 Maybe Any -> Any
v7 T_Tree_254
v8
  = T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
du_insertWith_296 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any
v6 Maybe Any -> Any
v7 T_Tree_254
v8
du_insertWith_296 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
du_insertWith_296 :: T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
du_insertWith_296 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 Maybe Any -> Any
v3 T_Tree_254
v4
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v4 of
      C_tree_262 Integer
v5 T_Tree_180
v6
        -> let v7 :: t
v7
                 = (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe
                     Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
                     ((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                        ((T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
                           T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_1036
 -> T_Value_38
 -> Any
 -> (Maybe Any -> Any)
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_818 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                              (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (Any -> Any
forall a b. a -> b
coe Any
v2) ((Maybe Any -> Any) -> Any
forall a b. a -> b
coe Maybe Any -> Any
v3) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v6)
                              ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                 Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                                    Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                    (T__'60''8331'__20 -> Any
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 -> Any
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 -> Any
forall a b. a -> b
coe Integer
v5)) in
           Any -> T_Tree_254
forall a b. a -> b
coe
             (Any -> Any -> Any
forall a b. a -> b
coe
                Any
forall a. a
v7
                (T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_1036
 -> T_Value_38
 -> Any
 -> (Maybe Any -> Any)
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_818 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                      (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (Any -> Any
forall a b. a -> b
coe Any
v2) ((Maybe Any -> Any) -> Any
forall a b. a -> b
coe Maybe Any -> Any
v3) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v6)
                      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                            Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                            (T__'60''8331'__20 -> Any
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 -> Any
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_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.delete
d_delete_304 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_254 -> T_Tree_254
d_delete_304 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> T_Tree_254
-> T_Tree_254
d_delete_304 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 Any
v6 T_Tree_254
v7 = T_StrictTotalOrder_1036 -> Any -> T_Tree_254 -> T_Tree_254
du_delete_304 T_StrictTotalOrder_1036
v3 Any
v6 T_Tree_254
v7
du_delete_304 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  AgdaAny -> T_Tree_254 -> T_Tree_254
du_delete_304 :: T_StrictTotalOrder_1036 -> Any -> T_Tree_254 -> T_Tree_254
du_delete_304 T_StrictTotalOrder_1036
v0 Any
v1 T_Tree_254
v2
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v2 of
      C_tree_262 Integer
v3 T_Tree_180
v4
        -> let v5 :: t
v5
                 = (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> t
forall a b. a -> b
coe
                     Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
                     ((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
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 -> Any) -> Any -> Any
forall a b. a -> b
coe
                           T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_1036
 -> Maybe (Maybe Any)
 -> Maybe (Maybe Any)
 -> Integer
 -> Any
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Integer
-> Any
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_936 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                              ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                 Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                 (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                              (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                              (Any -> Any
forall a b. a -> b
coe Any
v1) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v4)
                              ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                 Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                                    Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                    (T__'60''8331'__20 -> Any
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 -> Any
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 -> Any
forall a b. a -> b
coe Integer
v3)) in
           Any -> T_Tree_254
forall a b. a -> b
coe
             (Any -> Any -> Any
forall a b. a -> b
coe
                Any
forall a. a
v5
                (T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_1036
 -> Maybe (Maybe Any)
 -> Maybe (Maybe Any)
 -> Integer
 -> Any
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Integer
-> Any
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_936 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                      ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                         Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                         (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                      (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> Any
forall a b. a -> b
coe Integer
v3)
                      (Any -> Any
forall a b. a -> b
coe Any
v1) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v4)
                      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                            Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                            (T__'60''8331'__20 -> Any
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 -> Any
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_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.lookup
d_lookup_312 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> AgdaAny -> Maybe AgdaAny
d_lookup_312 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Any
-> Maybe Any
d_lookup_312 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 T_Tree_254
v6 Any
v7
  = T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 T_StrictTotalOrder_1036
v3 T_Value_38
v5 T_Tree_254
v6 Any
v7
du_lookup_312 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> AgdaAny -> Maybe AgdaAny
du_lookup_312 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Tree_254
v2 Any
v3
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v2 of
      C_tree_262 Integer
v4 T_Tree_180
v5
        -> (T_StrictTotalOrder_1036
 -> T_Value_38 -> T_Tree_180 -> Any -> T_Σ_14 -> Maybe Any)
-> Any -> Any -> Any -> Any -> Any -> Maybe Any
forall a b. a -> b
coe
             T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> Any -> T_Σ_14 -> Maybe Any
MAlonzo.Code.Data.Tree.AVL.Indexed.du_lookup_1034 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)
             (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v5) (Any -> Any
forall a b. a -> b
coe Any
v3)
             ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                   Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                   (T__'60''8331'__20 -> Any
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 -> Any
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_254
_ -> Maybe Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_330 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_330 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Val_330 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_332 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_332 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Wal_332 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.map
d_map_334 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
d_map_334 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
d_map_334 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 ~T_Value_38
v7 Any -> Any -> Any
v8 T_Tree_254
v9 = (Any -> Any -> Any) -> T_Tree_254 -> T_Tree_254
du_map_334 Any -> Any -> Any
v8 T_Tree_254
v9
du_map_334 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_254 -> T_Tree_254
du_map_334 :: (Any -> Any -> Any) -> T_Tree_254 -> T_Tree_254
du_map_334 Any -> Any -> Any
v0 T_Tree_254
v1
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v1 of
      C_tree_262 Integer
v2 T_Tree_180
v3
        -> (Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
             Integer -> T_Tree_180 -> T_Tree_254
C_tree_262 (Integer -> Any
forall a b. a -> b
coe Integer
v2)
             (((Any -> Any -> Any) -> T_Tree_180 -> T_Tree_180)
-> Any -> Any -> Any
forall a b. a -> b
coe
                (Any -> Any -> Any) -> T_Tree_180 -> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_map_1188 ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any
v0) (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v3))
      T_Tree_254
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_348 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_348 :: T_Value_38 -> Any -> ()
d_Val_348 = T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.member
d_member_350 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_254 -> Bool
d_member_350 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> T_Tree_254
-> Bool
d_member_350 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any
v6 T_Tree_254
v7
  = T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du_member_350 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any
v6 T_Tree_254
v7
du_member_350 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_254 -> Bool
du_member_350 :: T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du_member_350 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any
v2 T_Tree_254
v3
  = (Maybe Any -> Bool) -> Any -> Bool
forall a b. a -> b
coe
      Maybe Any -> Bool
MAlonzo.Code.Data.Maybe.Base.du_is'45'just_20
      ((T_StrictTotalOrder_1036
 -> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v3) (Any -> Any
forall a b. a -> b
coe Any
v2))
-- Data.Tree.AVL._.headTail
d_headTail_356 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_356 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Maybe T_Σ_14
d_headTail_356 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_headTail_356 T_StrictTotalOrder_1036
v3 T_Tree_254
v6
du_headTail_356 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_356 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_headTail_356 T_StrictTotalOrder_1036
v0 T_Tree_254
v1
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v1 of
      C_tree_262 Integer
v2 T_Tree_180
v3
        -> let v4 :: b
v4
                 = let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   Any -> b
forall a b. a -> b
coe
                     (let v5 :: t
v5
                            = (Integer -> T_Tree_180 -> T_Σ_14) -> Any -> Any -> t
forall a b. a -> b
coe
                                Integer -> T_Tree_180 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_headTail_648 (Integer -> Any
forall a b. a -> b
coe Integer
v4)
                                (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v3) in
                      Any -> Any
forall a b. a -> b
coe
                        (case Any -> T_Σ_14
forall a b. a -> b
coe Any
forall a. a
v5 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v6 Any
v7
                             -> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v7 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v8 Any
v9
                                    -> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v9 of
                                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v10 Any
v11
                                           -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                   Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (Any -> Any
forall a b. a -> b
coe Any
v6)
                                                   ((Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
                                                      ((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                                         (Any -> Any
forall a b. a -> b
coe Any
v10) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                      ((T_StrictTotalOrder_1036
 -> Maybe (Maybe Any)
 -> Maybe (Maybe Any)
 -> Maybe (Maybe Any)
 -> T__'60''8314'__20
 -> T_Tree_180
 -> T_Tree_180)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'737'_290
                                                         (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                                                         ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                            Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            (Maybe Any -> Any
forall a b. a -> b
coe
                                                               Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                                                         ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                            Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                               Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                               ((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe
                                                                  T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
                                                                  (Any -> Any
forall a b. a -> b
coe Any
v6))))
                                                         (Maybe Any -> Any
forall a b. a -> b
coe
                                                            Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                                                         ((Any -> T__'60''8314'__20) -> Any -> Any
forall a b. a -> b
coe
                                                            Any -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
                                                            (T__'60''8331'__20 -> Any
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))
                                                         (Any -> Any
forall a b. a -> b
coe Any
v11))))
                                         T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           Any -> Maybe T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v3 of
                MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_192 T__'60''8314'__20
v5
                  -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                T_Tree_180
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
      T_Tree_254
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.initLast
d_initLast_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_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_368 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Maybe T_Σ_14
d_initLast_368 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_initLast_368 T_StrictTotalOrder_1036
v3 T_Tree_254
v6
du_initLast_368 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  T_Tree_254 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_368 :: T_StrictTotalOrder_1036 -> T_Tree_254 -> Maybe T_Σ_14
du_initLast_368 T_StrictTotalOrder_1036
v0 T_Tree_254
v1
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v1 of
      C_tree_262 Integer
v2 T_Tree_180
v3
        -> let v4 :: b
v4
                 = let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   Any -> b
forall a b. a -> b
coe
                     (let v5 :: t
v5
                            = (Integer -> T_Tree_180 -> T_Σ_14) -> Any -> Any -> t
forall a b. a -> b
coe
                                Integer -> T_Tree_180 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_initLast_698 (Integer -> Any
forall a b. a -> b
coe Integer
v4)
                                (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v3) in
                      Any -> Any
forall a b. a -> b
coe
                        (case Any -> T_Σ_14
forall a b. a -> b
coe Any
forall a. a
v5 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v6 Any
v7
                             -> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v7 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v8 Any
v9
                                    -> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v9 of
                                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v10 Any
v11
                                           -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                   Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   ((Integer -> T_Tree_180 -> T_Tree_254) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      Integer -> T_Tree_180 -> T_Tree_254
C_tree_262
                                                      ((T_Fin_10 -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                                         (Any -> Any
forall a b. a -> b
coe Any
v10) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
                                                      ((T_StrictTotalOrder_1036
 -> Maybe (Maybe Any)
 -> Maybe (Maybe Any)
 -> Maybe (Maybe Any)
 -> T_Tree_180
 -> T__'60''8314'__20
 -> T_Tree_180)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                         T_StrictTotalOrder_1036
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> Maybe (Maybe Any)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'691'_316
                                                         (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                                                         ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                            Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            (Maybe Any -> Any
forall a b. a -> b
coe
                                                               Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                                                         ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                            Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                            ((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                                                               Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                               ((T_K'38'__56 -> Any) -> Any -> Any
forall a b. a -> b
coe
                                                                  T_K'38'__56 -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
                                                                  (Any -> Any
forall a b. a -> b
coe Any
v6))))
                                                         (Maybe Any -> Any
forall a b. a -> b
coe
                                                            Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                                                         (Any -> Any
forall a b. a -> b
coe Any
v11)
                                                         (T__'60''8314'__20 -> Any
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)))
                                                   (Any -> Any
forall a b. a -> b
coe Any
v6))
                                         T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           Any -> Maybe T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v3 of
                MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_192 T__'60''8314'__20
v5
                  -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                T_Tree_180
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4)
      T_Tree_254
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.foldr
d_foldr_382 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_254 -> AgdaAny
d_foldr_382 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> ()
-> ()
-> (Any -> Any -> Any -> Any)
-> Any
-> T_Tree_254
-> Any
d_foldr_382 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 ~()
v6 ~()
v7 Any -> Any -> Any -> Any
v8 Any
v9 T_Tree_254
v10
  = (Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382 Any -> Any -> Any -> Any
v8 Any
v9 T_Tree_254
v10
du_foldr_382 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_254 -> AgdaAny
du_foldr_382 :: (Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382 Any -> Any -> Any -> Any
v0 Any
v1 T_Tree_254
v2
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v2 of
      C_tree_262 Integer
v3 T_Tree_180
v4
        -> ((Any -> Any -> Any -> Any) -> Any -> T_Tree_180 -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
             (Any -> Any -> Any -> Any) -> Any -> T_Tree_180 -> Any
MAlonzo.Code.Data.Tree.AVL.Indexed.du_foldr_1114 ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v0) (Any -> Any
forall a b. a -> b
coe Any
v1)
             (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v4)
      T_Tree_254
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.fromList
d_fromList_390 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] -> T_Tree_254
d_fromList_390 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> [T_K'38'__56]
-> T_Tree_254
d_fromList_390 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_1036
-> T_Value_38 -> [T_K'38'__56] -> T_Tree_254
du_fromList_390 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_fromList_390 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] -> T_Tree_254
du_fromList_390 :: T_StrictTotalOrder_1036
-> T_Value_38 -> [T_K'38'__56] -> T_Tree_254
du_fromList_390 T_StrictTotalOrder_1036
v0 T_Value_38
v1
  = ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> [T_K'38'__56] -> T_Tree_254
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
      (((Any -> Any) -> (Any -> Any) -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
         (Any -> Any) -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Function.Base.du__'8728''8242'__216
         (((Any -> Any -> Any) -> T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> Any) -> T_Σ_14 -> Any
MAlonzo.Code.Data.Product.Base.du_uncurry_244
            ((T_StrictTotalOrder_1036
 -> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254)
-> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)))
         ((T_K'38'__56 -> T_Σ_14) -> Any
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80))
      (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
du_empty_274)
-- Data.Tree.AVL._.toList
d_toList_392 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_392 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> [T_K'38'__56]
d_toList_392 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_Tree_254 -> [T_K'38'__56]
du_toList_392 T_Tree_254
v6
du_toList_392 ::
  T_Tree_254 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_392 :: T_Tree_254 -> [T_K'38'__56]
du_toList_392 T_Tree_254
v0
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v0 of
      C_tree_262 Integer
v1 T_Tree_180
v2
        -> (([Any] -> [Any]) -> [Any]) -> Any -> [T_K'38'__56]
forall a b. a -> b
coe
             ([Any] -> [Any]) -> [Any]
MAlonzo.Code.Data.DifferenceList.du_toList_54
             ((T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]) -> Any -> Any
forall a b. a -> b
coe
                T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
MAlonzo.Code.Data.Tree.AVL.Indexed.du_toDiffList_1140 (T_Tree_180 -> Any
forall a b. a -> b
coe T_Tree_180
v2))
      T_Tree_254
_ -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.size
d_size_396 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> Integer
d_size_396 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> Integer
d_size_396 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_1036
v3 ~()
v4 ~T_Value_38
v5 T_Tree_254
v6 = T_Tree_254 -> Integer
du_size_396 T_Tree_254
v6
du_size_396 :: T_Tree_254 -> Integer
du_size_396 :: T_Tree_254 -> Integer
du_size_396 T_Tree_254
v0
  = case T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
v0 of
      C_tree_262 Integer
v1 T_Tree_180
v2
        -> (T_Tree_180 -> Integer) -> T_Tree_180 -> Integer
forall a b. a -> b
coe T_Tree_180 -> Integer
MAlonzo.Code.Data.Tree.AVL.Indexed.du_size_1164 T_Tree_180
v2
      T_Tree_254
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_412 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_412 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Val_412 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_414 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_414 :: T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
d_Wal_414 = T_StrictTotalOrder_1036
-> () -> () -> T_Value_38 -> T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.unionWith
d_unionWith_418 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_unionWith_418 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_unionWith_418 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 T_Value_38
v7 Any -> Any -> Maybe Any -> Any
v8 T_Tree_254
v9 T_Tree_254
v10
  = T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 T_StrictTotalOrder_1036
v3 T_Value_38
v7 Any -> Any -> Maybe Any -> Any
v8 T_Tree_254
v9 T_Tree_254
v10
du_unionWith_418 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_unionWith_418 :: T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any -> Any -> Maybe Any -> Any
v2 T_Tree_254
v3 T_Tree_254
v4
  = ((Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382
      ((Any -> Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v5 Any
v6 ->
            (T_StrictTotalOrder_1036
 -> T_Value_38
 -> Any
 -> (Maybe Any -> Any)
 -> T_Tree_254
 -> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> Any
-> (Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
du_insertWith_296 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (Any -> Any
forall a b. a -> b
coe Any
v5) ((Any -> Any -> Maybe Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Maybe Any -> Any
v2 Any
v5 Any
v6)))
      (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v4) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v3)
-- Data.Tree.AVL._.Val
d_Val_438 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_438 :: T_Value_38 -> Any -> ()
d_Val_438 = T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.union
d_union_440 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_union_440 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_union_440 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_440 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_union_440 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_440 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_union_440 T_StrictTotalOrder_1036
v0 T_Value_38
v1
  = (T_StrictTotalOrder_1036
 -> T_Value_38
 -> (Any -> Any -> Maybe Any -> Any)
 -> T_Tree_254
 -> T_Tree_254
 -> T_Tree_254)
-> Any -> Any -> Any -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
-- Data.Tree.AVL._.unionsWith
d_unionsWith_444 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  [T_Tree_254] -> T_Tree_254
d_unionsWith_444 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
d_unionsWith_444 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any -> Any -> Maybe Any -> Any
v6 [T_Tree_254]
v7
  = T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_444 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any -> Any -> Maybe Any -> Any
v6 [T_Tree_254]
v7
du_unionsWith_444 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  [T_Tree_254] -> T_Tree_254
du_unionsWith_444 :: T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_444 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any -> Any -> Maybe Any -> Any
v2 [T_Tree_254]
v3
  = ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
      (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((T_StrictTotalOrder_1036
 -> T_Value_38
 -> (Any -> Any -> Maybe Any -> Any)
 -> T_Tree_254
 -> T_Tree_254
 -> T_Tree_254)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_unionWith_418 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Maybe Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Maybe Any -> Any
v2))
      (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
du_empty_274) ([T_Tree_254] -> Any
forall a b. a -> b
coe [T_Tree_254]
v3)
-- Data.Tree.AVL._.unions
d_unions_450 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_254] -> T_Tree_254
d_unions_450 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> [T_Tree_254]
-> T_Tree_254
d_unions_450 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_unions_450 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_unions_450 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_254] -> T_Tree_254
du_unions_450 :: T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_unions_450 T_StrictTotalOrder_1036
v0 T_Value_38
v1
  = (T_StrictTotalOrder_1036
 -> T_Value_38
 -> (Any -> Any -> Maybe Any -> Any)
 -> [T_Tree_254]
 -> T_Tree_254)
-> Any -> Any -> Any -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Maybe Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_unionsWith_444 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
-- Data.Tree.AVL._.Val
d_Val_468 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_468 :: T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
d_Val_468 = T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_470 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_470 :: T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
d_Wal_470 = T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
forall a. a
erased
-- Data.Tree.AVL._.Xal
d_Xal_472 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Xal_472 :: T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
d_Xal_472 = T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> Any
-> ()
forall a. a
erased
-- Data.Tree.AVL._.intersectionWith
d_intersectionWith_476 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_intersectionWith_476 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_intersectionWith_476 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 T_Tree_254
v11
                       T_Tree_254
v12
  = T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 T_StrictTotalOrder_1036
v3 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 T_Tree_254
v11 T_Tree_254
v12
du_intersectionWith_476 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersectionWith_476 :: T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Value_38
v2 Any -> Any -> Any -> Any
v3 T_Tree_254
v4 T_Tree_254
v5
  = ((Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
      (Any -> Any -> Any -> Any) -> Any -> T_Tree_254 -> Any
du_foldr_382
      ((T_StrictTotalOrder_1036
 -> T_Value_38
 -> T_Value_38
 -> (Any -> Any -> Any -> Any)
 -> T_Tree_254
 -> Any
 -> Any
 -> T_Tree_254
 -> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
du_cons_490 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v2) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v3) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v5))
      (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
du_empty_274) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v4)
-- Data.Tree.AVL._._.cons
d_cons_490 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_254 ->
  T_Tree_254 -> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
d_cons_490 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
d_cons_490 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 ~T_Tree_254
v11 T_Tree_254
v12 Any
v13
           Any
v14
  = T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
du_cons_490 T_StrictTotalOrder_1036
v3 T_Value_38
v8 T_Value_38
v9 Any -> Any -> Any -> Any
v10 T_Tree_254
v12 Any
v13 Any
v14
du_cons_490 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_254 -> AgdaAny -> AgdaAny -> T_Tree_254 -> T_Tree_254
du_cons_490 :: T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
du_cons_490 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Value_38
v2 Any -> Any -> Any -> Any
v3 T_Tree_254
v4 Any
v5 Any
v6
  = let v7 :: t
v7 = (T_StrictTotalOrder_1036
 -> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any)
-> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> Any -> Maybe Any
du_lookup_312 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_254 -> Any
forall a b. a -> b
coe T_Tree_254
v4) (Any -> Any
forall a b. a -> b
coe Any
v5) in
    Any -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe
      (case Any -> Maybe Any
forall a b. a -> b
coe Any
forall a. a
v7 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v8
           -> (T_StrictTotalOrder_1036
 -> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                T_StrictTotalOrder_1036
-> T_Value_38 -> Any -> Any -> T_Tree_254 -> T_Tree_254
du_insert_286 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                (((Any -> Any -> Any -> Any -> Any) -> T_Value_38)
-> (Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                   (Any -> Any -> Any -> Any -> Any) -> T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.C_MkValue_50
                   (T_Value_38 -> Any -> Any -> Any -> Any -> Any
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> T_Value_38
forall a b. a -> b
coe T_Value_38
v2)))
                (Any -> Any
forall a b. a -> b
coe Any
v5) ((Any -> Any -> Any -> Any) -> Any -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v3 Any
v5 Any
v6 Any
v8)
         Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> (Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v8 -> Any
v8)
         Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL._.Val
d_Val_508 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_508 :: T_Value_38 -> Any -> ()
d_Val_508 = T_Value_38 -> Any -> ()
forall a. a
erased
-- Data.Tree.AVL._.intersection
d_intersection_510 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
d_intersection_510 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
d_intersection_510 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5
  = T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_510 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_intersection_510 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_510 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_254 -> T_Tree_254 -> T_Tree_254
du_intersection_510 T_StrictTotalOrder_1036
v0 T_Value_38
v1
  = (T_StrictTotalOrder_1036
 -> T_Value_38
 -> T_Value_38
 -> (Any -> Any -> Any -> Any)
 -> T_Tree_254
 -> T_Tree_254
 -> T_Tree_254)
-> Any
-> Any
-> Any
-> Any
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
forall a b. a -> b
coe
      T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)
      ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
-- Data.Tree.AVL._.intersectionsWith
d_intersectionsWith_514 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [T_Tree_254] -> T_Tree_254
d_intersectionsWith_514 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
d_intersectionsWith_514 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5 Any -> Any -> Any -> Any
v6 [T_Tree_254]
v7
  = T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_intersectionsWith_514 T_StrictTotalOrder_1036
v3 T_Value_38
v5 Any -> Any -> Any -> Any
v6 [T_Tree_254]
v7
du_intersectionsWith_514 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [T_Tree_254] -> T_Tree_254
du_intersectionsWith_514 :: T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_intersectionsWith_514 T_StrictTotalOrder_1036
v0 T_Value_38
v1 Any -> Any -> Any -> Any
v2 [T_Tree_254]
v3
  = case [T_Tree_254] -> [Any]
forall a b. a -> b
coe [T_Tree_254]
v3 of
      [] -> T_Tree_254 -> T_Tree_254
forall a b. a -> b
coe T_Tree_254
du_empty_274
      (:) Any
v4 [Any]
v5
        -> ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> T_Tree_254
forall a b. a -> b
coe
             (Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldl_230
             ((T_StrictTotalOrder_1036
 -> T_Value_38
 -> T_Value_38
 -> (Any -> Any -> Any -> Any)
 -> T_Tree_254
 -> T_Tree_254
 -> T_Tree_254)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> T_Value_38
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> T_Tree_254
-> T_Tree_254
-> T_Tree_254
du_intersectionWith_476 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe Any -> Any -> Any -> Any
v2))
             (Any -> Any
forall a b. a -> b
coe Any
v4) ([Any] -> Any
forall a b. a -> b
coe [Any]
v5)
      [Any]
_ -> T_Tree_254
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.intersections
d_intersections_524 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_254] -> T_Tree_254
d_intersections_524 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> [T_Tree_254]
-> T_Tree_254
d_intersections_524 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5
  = T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_intersections_524 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du_intersections_524 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_254] -> T_Tree_254
du_intersections_524 :: T_StrictTotalOrder_1036 -> T_Value_38 -> [T_Tree_254] -> T_Tree_254
du_intersections_524 T_StrictTotalOrder_1036
v0 T_Value_38
v1
  = (T_StrictTotalOrder_1036
 -> T_Value_38
 -> (Any -> Any -> Any -> Any)
 -> [T_Tree_254]
 -> T_Tree_254)
-> Any -> Any -> Any -> [T_Tree_254] -> T_Tree_254
forall a b. a -> b
coe
      T_StrictTotalOrder_1036
-> T_Value_38
-> (Any -> Any -> Any -> Any)
-> [T_Tree_254]
-> T_Tree_254
du_intersectionsWith_514 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1) ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v3))
-- Data.Tree.AVL._∈?_
d__'8712''63'__530 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_254 -> Bool
d__'8712''63'__530 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_1036
-> ()
-> T_Value_38
-> Any
-> T_Tree_254
-> Bool
d__'8712''63'__530 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_1036
v3 ~()
v4 T_Value_38
v5
  = T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du__'8712''63'__530 T_StrictTotalOrder_1036
v3 T_Value_38
v5
du__'8712''63'__530 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_254 -> Bool
du__'8712''63'__530 :: T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du__'8712''63'__530 T_StrictTotalOrder_1036
v0 T_Value_38
v1 = (T_StrictTotalOrder_1036
 -> T_Value_38 -> Any -> T_Tree_254 -> Bool)
-> Any -> Any -> Any -> T_Tree_254 -> Bool
forall a b. a -> b
coe T_StrictTotalOrder_1036 -> T_Value_38 -> Any -> T_Tree_254 -> Bool
du_member_350 (T_StrictTotalOrder_1036 -> Any
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> Any
forall a b. a -> b
coe T_Value_38
v1)