{-# 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.Indexed 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
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.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Tree.AVL.Height
import qualified MAlonzo.Code.Data.Tree.AVL.Key
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.Point.Equality
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures
d__'60'_'60'__102 ::
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 ->
Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
d__'60'_'60'__102 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
d__'60''8314'__104 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__104 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d__'8776''8729'__106 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__106 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Key'8314'_108 ::
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 -> ()
d_Key'8314'_108 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
d_Key'8314'_108 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
forall a. a
erased
d_irrefl'8314'_110 ::
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 ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_irrefl'8314'_110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
d_irrefl'8314'_110 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
forall a. a
erased
d_refl'8314'_112 ::
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 ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_112 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_112 T_StrictTotalOrder_1036
v3
du_refl'8314'_112 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_refl'8314'_112 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_112 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20)
-> AgdaAny -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_refl'8314'_94 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
d_strictPartialOrder_114 ::
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.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_strictPartialOrder_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_StrictPartialOrder_556
d_strictPartialOrder_114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3
= T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
du_strictPartialOrder_114 T_StrictTotalOrder_1036
v3
du_strictPartialOrder_114 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
du_strictPartialOrder_114 :: T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
du_strictPartialOrder_114 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556)
-> AgdaAny -> T_StrictPartialOrder_556
forall a b. a -> b
coe
T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
MAlonzo.Code.Data.Tree.AVL.Key.du_strictPartialOrder_118 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
d_strictTotalOrder_116 ::
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.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_strictTotalOrder_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_StrictTotalOrder_1036
d_strictTotalOrder_116 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_strictTotalOrder_116 T_StrictTotalOrder_1036
v3
du_strictTotalOrder_116 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
du_strictTotalOrder_116 :: T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_strictTotalOrder_116 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036)
-> AgdaAny -> T_StrictTotalOrder_1036
forall a b. a -> b
coe
T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
MAlonzo.Code.Data.Tree.AVL.Key.du_strictTotalOrder_202 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
d_sym'8314'_118 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_sym'8314'_118 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_sym'8314'_118 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_118 T_StrictTotalOrder_1036
v3
du_sym'8314'_118 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_sym'8314'_118 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_118 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_sym'8314'_100 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
d_trans'8314'_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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_trans'8314'_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_trans'8314'_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_120 T_StrictTotalOrder_1036
v3
du_trans'8314'_120 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_trans'8314'_120 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_120 T_StrictTotalOrder_1036
v0
= (T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
d_'8869''8314''60''91'_'93''60''8868''8314'_122 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_122 :: T_StrictTotalOrder_1036 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_122 ~T_StrictTotalOrder_1036
v0 ~AgdaAny
v1
= T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_122
du_'8869''8314''60''91'_'93''60''8868''8314'_122 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_122 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_122
= (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
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)
d_'91'_'93''45'injective_138 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'_'93''45'injective_138 :: T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'91'_'93''45'injective_138 = T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_K'38'__144 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_K'38'__144 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Value_148 :: p -> p -> p -> p -> p -> T_Level_18
d_Value_148 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
d_const_150 ::
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_150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
d_const_150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 = T_Level_18 -> T_Level_18 -> T_Value_38
du_const_150
du_const_150 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_150 :: T_Level_18 -> T_Level_18 -> T_Value_38
du_const_150 T_Level_18
v0 T_Level_18
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
d_fromPair_152 ::
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_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 = T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_152
du_fromPair_152 ::
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_152 :: T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_152 T_Level_18
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
d_key_154 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_154 :: T_K'38'__56 -> AgdaAny
d_key_154 T_K'38'__56
v0
= (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
d_toPair_156 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_156 :: T_K'38'__56 -> T_Σ_14
d_toPair_156 T_K'38'__56
v0
= (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0))
((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0))
d_value_158 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_158 :: T_K'38'__56 -> AgdaAny
d_value_158 T_K'38'__56
v0
= (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
d_key_162 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_162 :: T_K'38'__56 -> AgdaAny
d_key_162 T_K'38'__56
v0
= (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
d_value_164 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_164 :: T_K'38'__56 -> AgdaAny
d_value_164 T_K'38'__56
v0
= (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
d_family_168 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_168 :: T_Value_38 -> AgdaAny -> T_Level_18
d_family_168 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
d_respects_170 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_170 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_170 T_Value_38
v0
= (T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v0)
d_Tree_180 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_Tree_180 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T_Tree_180
= C_leaf_192 MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 |
C_node_208 Integer Integer
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 T_Tree_180 T_Tree_180
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30
d_ordered_224 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_180 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_ordered_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T__'60''8314'__20
d_ordered_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9
= T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 T_Tree_180
v9
du_ordered_224 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
T_Tree_180 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_ordered_224 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 T_Tree_180
v3
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v3 of
C_leaf_192 T__'60''8314'__20
v4 -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v4
C_node_208 Integer
v4 Integer
v5 T_K'38'__56
v7 T_Tree_180
v8 T_Tree_180
v9 T__'8764'_'8852'__30
v10
-> (T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20)
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'60''8314'__20
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1
((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'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
Maybe (Maybe AgdaAny)
v2
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
((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'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8))
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
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
((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'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
(Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v9))
T_Tree_180
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_236 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_236 :: T_Value_38 -> AgdaAny -> T_Level_18
d_Val_236 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
d_V'8776'_238 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_238 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_238 T_Value_38
v0
= (T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v0)
d_leaf'45'injective_248 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_leaf'45'injective_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
-> T__'8801'__12
d_leaf'45'injective_248 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_node'45'injective'45'key_280 ::
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 ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
T_Tree_180 ->
T_Tree_180 ->
T_Tree_180 ->
T_Tree_180 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_node'45'injective'45'key_280 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__56
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
d_node'45'injective'45'key_280 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__56
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_cast'737'_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_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_180 -> T_Tree_180
d_cast'737'_290 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
d_cast'737'_290 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T__'60''8314'__20
v10 T_Tree_180
v11
= T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
du_cast'737'_290 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T__'60''8314'__20
v10 T_Tree_180
v11
du_cast'737'_290 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_180 -> T_Tree_180
du_cast'737'_290 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
du_cast'737'_290 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4 T_Tree_180
v5
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v5 of
C_leaf_192 T__'60''8314'__20
v6
-> (T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> T_Tree_180
forall a b. a -> b
coe
T__'60''8314'__20 -> T_Tree_180
C_leaf_192
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20)
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4
T__'60''8314'__20
v6)
C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
du_cast'737'_290 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
((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'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9))))
(T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v4) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10))
T_Tree_180
v11 T__'8764'_'8852'__30
v12
T_Tree_180
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
d_cast'691'_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_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_180 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_180
d_cast'691'_316 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
d_cast'691'_316 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T_Tree_180
v10 T__'60''8314'__20
v11
= T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T_Tree_180
v10 T__'60''8314'__20
v11
du_cast'691'_316 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
T_Tree_180 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_180
du_cast'691'_316 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T_Tree_180
v4 T__'60''8314'__20
v5
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v4 of
C_leaf_192 T__'60''8314'__20
v6
-> (T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> T_Tree_180
forall a b. a -> b
coe
T__'60''8314'__20 -> T_Tree_180
C_leaf_192
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20)
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v6
T__'60''8314'__20
v5)
C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_180
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
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
((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'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9))))
(Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11) (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v5))
T__'8764'_'8852'__30
v12
T_Tree_180
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join'737''8314'_366 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
T_Tree_180 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8314'_366 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8314'_366 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
du_join'737''8314'_366 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
T_Tree_180 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8314'_366 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_180
v4 T__'8764'_'8852'__30
v5
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
(case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v0 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> case AgdaAny -> T_Tree_180
forall a b. a -> b
coe AgdaAny
v7 of
C_node_208 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_180
v15 T_Tree_180
v16 T__'8764'_'8852'__30
v17
-> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v17 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
-> case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v16 of
C_node_208 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_180
v23 T_Tree_180
v24 T__'8764'_'8852'__30
v25
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v22
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v1 Integer
v19 T_K'38'__56
v14 T_Tree_180
v15 T_Tree_180
v23
((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_max'8764'_50
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v20 Integer
v1 T_K'38'__56
v2 T_Tree_180
v24 T_Tree_180
v4
((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_'8764'max_58
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v14 T_Tree_180
v15
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
Integer
v1 T_K'38'__56
v2 T_Tree_180
v16 T_Tree_180
v4
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v14 T_Tree_180
v15
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v1 Integer
v1 T_K'38'__56
v2 T_Tree_180
v16 T_Tree_180
v4
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join'691''8314'_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_1036 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'691''8314'_456 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8314'_456 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8314'_456 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'691''8314'_456 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_180
v3 T_Σ_14
v4 T__'8764'_'8852'__30
v5
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
(case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
-> case AgdaAny -> T_Tree_180
forall a b. a -> b
coe AgdaAny
v7 of
C_node_208 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_180
v15 T_Tree_180
v16 T__'8764'_'8852'__30
v17
-> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v17 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v14
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0 Integer
v0 T_K'38'__56
v2 T_Tree_180
v3 T_Tree_180
v15
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T_Tree_180
v16
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v14
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v2 T_Tree_180
v3 T_Tree_180
v15
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
T_Tree_180
v16
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v15 of
C_node_208 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_180
v23 T_Tree_180
v24 T__'8764'_'8852'__30
v25
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
(Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v22
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0 Integer
v19 T_K'38'__56
v2 T_Tree_180
v3 T_Tree_180
v23
((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_max'8764'_50
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v20 Integer
v0 T_K'38'__56
v14 T_Tree_180
v24 T_Tree_180
v16
((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_'8764'max_58
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join'737''8315'_532 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
T_Tree_180 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8315'_532 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8315'_532 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
du_join'737''8315'_532 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
T_Tree_180 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8315'_532 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_180
v4 T__'8764'_'8852'__30
v5
= case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
Integer
0 -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
((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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4 T__'8764'_'8852'__30
v5))
T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ -> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
-> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v7 of
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
-> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456
((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_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0))
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)
((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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v4))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34)
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v0 T_K'38'__56
v2 AgdaAny
v8 T_Tree_180
v4
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v6 T_K'38'__56
v2 AgdaAny
v8 T_Tree_180
v4
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v10
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v10)
((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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 T_K'38'__56
v2 AgdaAny
v8 T_Tree_180
v4 T__'8764'_'8852'__30
v5))
T_Fin_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_join'691''8315'_594 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'691''8315'_594 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8315'_594 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8315'_594 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'691''8315'_594 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_180
v3 T_Σ_14
v4 T__'8764'_'8852'__30
v5
= case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
0 -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
((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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5))
T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
Integer
_ -> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
-> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v7 of
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
-> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v8
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v1
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v8
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
((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_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1))
(T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v2)
((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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v3))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42)
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v10
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v10)
((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
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
(T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v8 T__'8764'_'8852'__30
v5))
T_Fin_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_headTail_648 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_648 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T_Σ_14
d_headTail_648 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_180
v9
= Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 Integer
v8 T_Tree_180
v9
du_headTail_648 ::
Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_648 :: Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 Integer
v0 T_Tree_180
v1
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1 of
C_node_208 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_180
v6 T_Tree_180
v7 T__'8764'_'8852'__30
v8
-> let v9 :: b
v9
= let v9 :: Integer
v9 = 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 -> b
forall a b. a -> b
coe
(let v10 :: t
v10 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v11 AgdaAny
v12
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v12 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
-> (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
v11)
((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
v13)
((Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v6 of
C_leaf_192 T__'60''8314'__20
v10
-> let v11 :: b
v11
= case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2 of
AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
let v11 :: Integer
v11 = 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 -> b
forall a b. a -> b
coe
(let v12 :: t
v12 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v14 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
-> (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
v13)
((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
v15)
((Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v9 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v8 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
-> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0 of
AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3 of
AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
(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 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
((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
(T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
((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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)))
AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
((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 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
((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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)))
T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
T_Tree_180
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_initLast_698 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_698 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T_Σ_14
d_initLast_698 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_180
v9
= Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 Integer
v8 T_Tree_180
v9
du_initLast_698 ::
Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_698 :: Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 Integer
v0 T_Tree_180
v1
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1 of
C_node_208 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_180
v6 T_Tree_180
v7 T__'8764'_'8852'__30
v8
-> let v9 :: b
v9
= let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> b
forall a b. a -> b
coe
(let v10 :: t
v10 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v11 AgdaAny
v12
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v12 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
-> (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
v11)
((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
v13)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v7 of
C_leaf_192 T__'60''8314'__20
v10
-> let v11 :: b
v11
= case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3 of
AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> b
forall a b. a -> b
coe
(let v12 :: t
v12 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v14 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
-> (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
v13)
((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
v15)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16)
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v9 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v8 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
((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 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
((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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6)))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0 of
AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
(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 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
((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 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
((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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6)))
AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
T_Tree_180
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join_754 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
T_Tree_180 ->
T_Tree_180 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join_754 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join_754 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_180
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
= T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_754 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_180
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
du_join_754 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
T_Tree_180 ->
T_Tree_180 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join_754 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_754 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 Integer
v4 Integer
v5 Integer
v6 T_Tree_180
v7 T_Tree_180
v8 T__'8764'_'8852'__30
v9
= let v10 :: b
v10
= let v10 :: Integer
v10 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> b
forall a b. a -> b
coe
(let v11 :: t
v11 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v10) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v11 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v12 AgdaAny
v13
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v13 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12)
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
((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'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v9)
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v8 of
C_leaf_192 T__'60''8314'__20
v11
-> let v12 :: b
v12
= case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5 of
AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
let v12 :: Integer
v12 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> b
forall a b. a -> b
coe
(let v13 :: t
v13 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v13 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v15 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v16 AgdaAny
v17
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
((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'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v9)
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v10 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v9 of
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
(T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v11))
T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
-> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6 of
AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
(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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
(T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v11))
AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12
T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12)
T_Tree_180
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10)
d_empty_790 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_180
d_empty_790 :: T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
d_empty_790 ~T_Value_38
v0 ~Maybe (Maybe AgdaAny)
v1 ~Maybe (Maybe AgdaAny)
v2 = T__'60''8314'__20 -> T_Tree_180
du_empty_790
du_empty_790 ::
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_180
du_empty_790 :: T__'60''8314'__20 -> T_Tree_180
du_empty_790 = (T__'60''8314'__20 -> T_Tree_180)
-> T__'60''8314'__20 -> T_Tree_180
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_180
C_leaf_192
d_singleton_798 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_180
d_singleton_798 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Tree_180
d_singleton_798 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
= AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180
du_singleton_798 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
du_singleton_798 ::
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_180
du_singleton_798 :: AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180
du_singleton_798 AgdaAny
v0 AgdaAny
v1 T_Σ_14
v2
= case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_180
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer
0 :: Integer) (Integer
0 :: Integer)
((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
((T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_180
C_leaf_192 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)) ((T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_180
C_leaf_192 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38)
T_Σ_14
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
d_insertWith_818 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insertWith_818 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
d_insertWith_818 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_180
v11 T_Σ_14
v12
= T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 T_StrictTotalOrder_1036
v3 T_Value_38
v5 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_180
v11 T_Σ_14
v12
du_insertWith_818 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insertWith_818 :: T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 T_StrictTotalOrder_1036
v0 T_Value_38
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_180
v4 T_Σ_14
v5
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v4 of
C_leaf_192 T__'60''8314'__20
v6
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180
du_singleton_798 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
((Maybe AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
(T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v5))
C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12
-> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v9 of
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v13 AgdaAny
v14
-> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v5 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
-> let v17 :: t
v17
= (T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544
(T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
(T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0))
AgdaAny
v2 AgdaAny
v13 in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v18
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9)
((T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
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_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10)
((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
v15)
((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
((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
AgdaAny
v18))))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v12)
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v19
-> (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
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6 Integer
v7
((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
((T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 T_Value_38
v1 AgdaAny
v2
AgdaAny
v13 AgdaAny
v19
((Maybe AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Maybe AgdaAny -> AgdaAny
v3
((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_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48
T_Value_38
v1 AgdaAny
v13 AgdaAny
v2
(let v21 :: t
v21
= (T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638)
-> AgdaAny -> t
forall a b. a -> b
coe
T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638
MAlonzo.Code.Relation.Binary.Bundles.du_decStrictPartialOrder_1098
(T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v22 :: t
v22
= (T_DecStrictPartialOrder_638 -> T_DecSetoid_84) -> AgdaAny -> t
forall a b. a -> b
coe
T_DecStrictPartialOrder_638 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.du_decSetoid_728
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v21) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v23 :: t
v23
= (T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe
T_DecSetoid_84 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_108
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v22) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
(T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
(AgdaAny -> T_Setoid_44
forall a b. a -> b
coe AgdaAny
forall a. a
v23))
AgdaAny
v2 AgdaAny
v13 AgdaAny
v19))))
AgdaAny
v14)))))
T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12)
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v20
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10)
((T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
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_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11)
((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
((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
AgdaAny
v20))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16)))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v12)
T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_K'38'__56
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_insert_920 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
AgdaAny ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insert_920 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
d_insert_920 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 AgdaAny
v10
= T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insert_920 T_StrictTotalOrder_1036
v3 T_Value_38
v5 AgdaAny
v9 AgdaAny
v10
du_insert_920 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny ->
AgdaAny ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insert_920 :: T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insert_920 T_StrictTotalOrder_1036
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3
= (T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v3))
d_delete_936 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_delete_936 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
d_delete_936 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_180
v10 T_Σ_14
v11
= T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_180
v10 T_Σ_14
v11
du_delete_936 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
T_Tree_180 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_delete_936 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Integer
v3 AgdaAny
v4 T_Tree_180
v5 T_Σ_14
v6
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v5 of
C_leaf_192 T__'60''8314'__20
v7
-> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v5)
C_node_208 Integer
v7 Integer
v8 T_K'38'__56
v10 T_Tree_180
v11 T_Tree_180
v12 T__'8764'_'8852'__30
v13
-> let v14 :: Integer
v14 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v10 of
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v15 AgdaAny
v16
-> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v6 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v17 AgdaAny
v18
-> let v19 :: t
v19
= (T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544
(T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
(T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0))
AgdaAny
v15 AgdaAny
v4 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v20
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v10) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11)
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
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
((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
forall a b. a -> b
coe AgdaAny
v15)))
(Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v12)
((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
((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
AgdaAny
v20))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v18)))
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v21
-> (T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_754 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
((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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
(Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v14) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v12)
(T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v22
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v10)
((T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
((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
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11)
((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
v17)
((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
((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
AgdaAny
v22))))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v12) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_lookup_1034 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_180 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
d_lookup_1034 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> AgdaAny
-> T_Σ_14
-> Maybe AgdaAny
d_lookup_1034 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9 AgdaAny
v10 T_Σ_14
v11
= T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 T_StrictTotalOrder_1036
v3 T_Value_38
v5 T_Tree_180
v9 AgdaAny
v10 T_Σ_14
v11
du_lookup_1034 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
T_Tree_180 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Tree_180
v2 AgdaAny
v3 T_Σ_14
v4
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v2 of
C_leaf_192 T__'60''8314'__20
v5 -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
C_node_208 Integer
v5 Integer
v6 T_K'38'__56
v8 T_Tree_180
v9 T_Tree_180
v10 T__'8764'_'8852'__30
v11
-> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v8 of
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v12 AgdaAny
v13
-> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
-> let v16 :: t
v16
= (T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544
(T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
(T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0))
AgdaAny
v12 AgdaAny
v3 in
AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v17
-> (T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10) (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
((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
AgdaAny
v17))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15))
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v18
-> (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_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 T_Value_38
v1 AgdaAny
v12 AgdaAny
v3 AgdaAny
v18
AgdaAny
v13)
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v19
-> (T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v9) (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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
((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
((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
AgdaAny
v19)))
T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Σ_14
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_K'38'__56
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_180
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_foldr_1114 ::
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 ->
() ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> T_Tree_180 -> AgdaAny
d_foldr_1114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> T_Level_18
-> T_Level_18
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_180
-> AgdaAny
d_foldr_1114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~Maybe (Maybe AgdaAny)
v8 ~Maybe (Maybe AgdaAny)
v9 ~Integer
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12
T_Tree_180
v13
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 T_Tree_180
v13
du_foldr_1114 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_180
v2
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v2 of
C_leaf_192 T__'60''8314'__20
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
C_node_208 Integer
v3 Integer
v4 T_K'38'__56
v6 T_Tree_180
v7 T_Tree_180
v8 T__'8764'_'8852'__30
v9
-> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v6 of
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v10 AgdaAny
v11
-> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0)
((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v10 AgdaAny
v11 (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 ((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_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8)))
(T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toDiffList_1140 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_180 ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toDiffList_1140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> [T_K'38'__56]
-> [T_K'38'__56]
d_toDiffList_1140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9
= T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 T_Tree_180
v9
du_toDiffList_1140 ::
T_Tree_180 ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toDiffList_1140 :: T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 T_Tree_180
v0
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v0 of
C_leaf_192 T__'60''8314'__20
v1 -> (AgdaAny -> AgdaAny) -> [T_K'38'__56] -> [T_K'38'__56]
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)
C_node_208 Integer
v1 Integer
v2 T_K'38'__56
v4 T_Tree_180
v5 T_Tree_180
v6 T__'8764'_'8852'__30
v7
-> (([AgdaAny] -> [AgdaAny])
-> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_K'38'__56] -> [T_K'38'__56]
forall a b. a -> b
coe
([AgdaAny] -> [AgdaAny])
-> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'43''43'__38
((T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v5))
((AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> T_K'38'__56 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'8759'__28 T_K'38'__56
v4
((T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6)))
T_Tree_180
_ -> [T_K'38'__56] -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toList_1154 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_180 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_1154 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> [T_K'38'__56]
d_toList_1154 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9
= T_Tree_180 -> [T_K'38'__56]
du_toList_1154 T_Tree_180
v9
du_toList_1154 ::
T_Tree_180 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_1154 :: T_Tree_180 -> [T_K'38'__56]
du_toList_1154 T_Tree_180
v0
= (T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56])
-> T_Tree_180 -> AgdaAny -> [T_K'38'__56]
forall a b. a -> b
coe
T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 T_Tree_180
v0
([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
d_size_1164 ::
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 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) -> Integer -> T_Tree_180 -> Integer
d_size_1164 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> Integer
d_size_1164 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 = T_Tree_180 -> Integer
du_size_1164
du_size_1164 :: T_Tree_180 -> Integer
du_size_1164 :: T_Tree_180 -> Integer
du_size_1164
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_180 -> Integer
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
(([AgdaAny] -> Integer) -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> Integer
MAlonzo.Code.Data.List.Base.du_length_284)
((T_Tree_180 -> [T_K'38'__56]) -> AgdaAny
forall a b. a -> b
coe T_Tree_180 -> [T_K'38'__56]
du_toList_1154)
d_Val_1178 ::
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_1178 :: T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Val_1178 = T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_Wal_1180 ::
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_1180 :: T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Wal_1180 = T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_map_1188 ::
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) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) -> Integer -> T_Tree_180 -> T_Tree_180
d_map_1188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T_Tree_180
d_map_1188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Value_38
v6 ~T_Value_38
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 ~Maybe (Maybe AgdaAny)
v9 ~Maybe (Maybe AgdaAny)
v10 ~Integer
v11 T_Tree_180
v12
= (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_180
v12
du_map_1188 ::
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_180
v1
= case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1 of
C_leaf_192 T__'60''8314'__20
v2 -> T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1
C_node_208 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_180
v6 T_Tree_180
v7 T__'8764'_'8852'__30
v8
-> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v5 of
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v9 AgdaAny
v10
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_180
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v2 Integer
v3
((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v9 AgdaAny
v10))
(((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6))
(((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)) T__'8764'_'8852'__30
v8
T_K'38'__56
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_180
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError