{-# 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.Empty
import qualified MAlonzo.Code.Data.Fin.Base
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'__88 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
d__'60'_'60'__88 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
d__'60''8314'__90 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__90 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d__'8776''8729'__92 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__92 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Key'8314'_94 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 -> ()
d_Key'8314'_94 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_864 -> T_Level_18
d_Key'8314'_94 = T_Level_18
-> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_864 -> T_Level_18
forall a. a
erased
d_irrefl'8314'_96 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_irrefl'8314'_96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_'8869'_4
d_irrefl'8314'_96 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_'8869'_4
forall a. a
erased
d_refl'8314'_98 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_98 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_98 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_98 T_StrictTotalOrder_864
v3
du_refl'8314'_98 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_refl'8314'_98 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_98 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20)
-> AgdaAny -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
forall a b. a -> b
coe T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_refl'8314'_88 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
d_strictPartialOrder_100 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_strictPartialOrder_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_StrictPartialOrder_472
d_strictPartialOrder_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3
= T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
du_strictPartialOrder_100 T_StrictTotalOrder_864
v3
du_strictPartialOrder_100 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
du_strictPartialOrder_100 :: T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
du_strictPartialOrder_100 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864 -> T_StrictPartialOrder_472)
-> AgdaAny -> T_StrictPartialOrder_472
forall a b. a -> b
coe
T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
MAlonzo.Code.Data.Tree.AVL.Key.du_strictPartialOrder_112 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
d_strictTotalOrder_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_864 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_strictTotalOrder_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_StrictTotalOrder_864
d_strictTotalOrder_102 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_strictTotalOrder_102 T_StrictTotalOrder_864
v3
du_strictTotalOrder_102 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
du_strictTotalOrder_102 :: T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_strictTotalOrder_102 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864 -> T_StrictTotalOrder_864)
-> AgdaAny -> T_StrictTotalOrder_864
forall a b. a -> b
coe
T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
MAlonzo.Code.Data.Tree.AVL.Key.du_strictTotalOrder_182 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
d_sym'8314'_104 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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'_104 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_sym'8314'_104 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_104 T_StrictTotalOrder_864
v3
du_sym'8314'_104 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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'_104 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_104 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> 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_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_sym'8314'_94 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
d_trans'8314'_106 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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'_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_trans'8314'_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_106 T_StrictTotalOrder_864
v3
du_trans'8314'_106 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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'_106 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_106 T_StrictTotalOrder_864
v0
= (T_StrictTotalOrder_864
-> 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_864
-> 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'_102 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)
d_'8869''8314''60''91'_'93''60''8868''8314'_108 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_108 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_108 ~T_StrictTotalOrder_864
v0 ~AgdaAny
v1
= T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_108
du_'8869''8314''60''91'_'93''60''8868''8314'_108 ::
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_108 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_108
= (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_124 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_124 :: T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'91'_'93''45'injective_124 = T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_K'38'__130 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_K'38'__130 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Value_134 :: p -> p -> p -> p -> p -> T_Level_18
d_Value_134 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
d_const_136 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
d_const_136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
d_const_136 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 = T_Level_18 -> T_Level_18 -> T_Value_38
du_const_136
du_const_136 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_136 :: T_Level_18 -> T_Level_18 -> T_Value_38
du_const_136 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_138 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
d_fromPair_138 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_138 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 = T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_138
du_fromPair_138 ::
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_138 :: T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_138 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_140 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_140 :: T_K'38'__56 -> AgdaAny
d_key_140 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_142 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_142 :: T_K'38'__56 -> T_Σ_14
d_toPair_142 = (T_K'38'__56 -> T_Σ_14) -> T_K'38'__56 -> T_Σ_14
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80
d_value_144 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_144 :: T_K'38'__56 -> AgdaAny
d_value_144 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_148 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_148 :: T_K'38'__56 -> AgdaAny
d_key_148 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_150 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_150 :: T_K'38'__56 -> AgdaAny
d_value_150 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_154 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_154 :: T_Value_38 -> AgdaAny -> T_Level_18
d_family_154 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
d_respects_156 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_156 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_156 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_166 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_Tree_166 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T_Tree_166
= C_leaf_178 MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 |
C_node_194 Integer Integer
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 T_Tree_166 T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30
d_ordered_210 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_166 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_ordered_210 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T__'60''8314'__20
d_ordered_210 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_166
v9
= T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 T_Tree_166
v9
du_ordered_210 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
T_Tree_166 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_ordered_210 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 T_Tree_166
v3
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
C_leaf_178 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_194 Integer
v4 Integer
v5 T_K'38'__56
v7 T_Tree_166
v8 T_Tree_166
v9 T__'8764'_'8852'__30
v10
-> (T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20)
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'60''8314'__20
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> 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'_102 T_StrictTotalOrder_864
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_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v8))
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
du_ordered_210 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v9))
T_Tree_166
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Val_222 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_222 :: T_Value_38 -> AgdaAny -> T_Level_18
d_Val_222 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
d_V'8776'_224 ::
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_224 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_224 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_234 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
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_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> 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_234 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> 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_266 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_166 ->
T_Tree_166 ->
T_Tree_166 ->
T_Tree_166 ->
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_266 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> 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_166
-> T_Tree_166
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
d_node'45'injective'45'key_266 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> 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_166
-> T_Tree_166
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_cast'737'_276 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.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_166 -> T_Tree_166
d_cast'737'_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
d_cast'737'_276 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
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_166
v11
= T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
du_cast'737'_276 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T__'60''8314'__20
v10 T_Tree_166
v11
du_cast'737'_276 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_166 -> T_Tree_166
du_cast'737'_276 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
du_cast'737'_276 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4 T_Tree_166
v5
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v5 of
C_leaf_178 T__'60''8314'__20
v6
-> (T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> T_Tree_166
forall a b. a -> b
coe
T__'60''8314'__20 -> T_Tree_166
C_leaf_178
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20)
-> T_StrictTotalOrder_864
-> 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_864
-> 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'_102 T_StrictTotalOrder_864
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_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10 T_Tree_166
v11 T__'8764'_'8852'__30
v12
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v6 Integer
v7 T_K'38'__56
v9
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
du_cast'737'_276 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v10))
T_Tree_166
v11 T__'8764'_'8852'__30
v12
T_Tree_166
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError
d_cast'691'_302 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_166 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_166
d_cast'691'_302 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
d_cast'691'_302 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
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_166
v10 T__'60''8314'__20
v11
= T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T_Tree_166
v10 T__'60''8314'__20
v11
du_cast'691'_302 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
T_Tree_166 ->
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_166
du_cast'691'_302 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T_Tree_166
v4 T__'60''8314'__20
v5
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v4 of
C_leaf_178 T__'60''8314'__20
v6
-> (T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> T_Tree_166
forall a b. a -> b
coe
T__'60''8314'__20 -> T_Tree_166
C_leaf_178
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20)
-> T_StrictTotalOrder_864
-> 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_864
-> 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'_102 T_StrictTotalOrder_864
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_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10 T_Tree_166
v11 T__'8764'_'8852'__30
v12
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_166
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11) (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v5))
T__'8764'_'8852'__30
v12
T_Tree_166
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join'737''8314'_352 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.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_166 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8314'_352 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8314'_352 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
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_166
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
du_join'737''8314'_352 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
T_Tree_166 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8314'_352 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_166
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_6
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
-> (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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(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_166
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v0 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
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_166
forall a b. a -> b
coe AgdaAny
v7 of
C_node_194 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_166
v15 T_Tree_166
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_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v16 of
C_node_194 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_166
v23 T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v1 Integer
v19 T_K'38'__56
v14 T_Tree_166
v15 T_Tree_166
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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v20 Integer
v1 T_K'38'__56
v2 T_Tree_166
v24 T_Tree_166
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_166
_ -> 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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (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_166
v15
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (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_166
v16 T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (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_166
v15
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v1 Integer
v1 T_K'38'__56
v2 T_Tree_166
v16 T_Tree_166
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_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Fin_6
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join'691''8314'_442 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.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_166 ->
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'_442 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8314'_442 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
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_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8314'_442 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
T_Tree_166 ->
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'_442 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_166
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_6
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
-> (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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
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_166
forall a b. a -> b
coe AgdaAny
v7 of
C_node_194 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_166
v15 T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0 Integer
v0 T_K'38'__56
v2 T_Tree_166
v3 T_Tree_166
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_166
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 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_166
v3 T_Tree_166
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_166
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_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v15 of
C_node_194 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_166
v23 T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0 Integer
v19 T_K'38'__56
v2 T_Tree_166
v3 T_Tree_166
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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v20 Integer
v0 T_K'38'__56
v14 T_Tree_166
v24 T_Tree_166
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_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_166
_ -> 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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
T_K'38'__56
v2 T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (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_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_166
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_6
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join'737''8315'_518 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.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_166 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8315'_518 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8315'_518 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
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_166
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
du_join'737''8315'_518 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
T_Tree_166 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8315'_518 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_166
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_6
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
-> (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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_166
v4 T__'8764'_'8852'__30
v5))
T_Fin_6
_ -> 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_6
forall a b. a -> b
coe AgdaAny
v7 of
T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
-> 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_166
-> 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_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442
((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v0 T_K'38'__56
v2 AgdaAny
v8 T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v6 T_K'38'__56
v2 AgdaAny
v8 T_Tree_166
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_6
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(Integer -> Integer
forall a b. a -> b
coe Integer
v0))
Integer
v1 T_K'38'__56
v2 AgdaAny
v8 T_Tree_166
v4 T__'8764'_'8852'__30
v5))
T_Fin_6
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_join'691''8315'_580 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.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_166 ->
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'_580 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8315'_580 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
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_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
= Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_166
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8315'_580 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
T_Tree_166 ->
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'_580 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_166
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_6
forall a b. a -> b
coe AgdaAny
v6 of
T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
-> (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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_6
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5))
T_Fin_6
_ -> 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_6
forall a b. a -> b
coe AgdaAny
v7 of
T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10
-> 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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v6
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_166
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v1
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> T_Fin_6
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_166
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_166
-> 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_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 Integer
v0
(T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
((T_Fin_6 -> T_Fin_6) -> AgdaAny -> T_Fin_6
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
(Integer -> Integer
forall a b. a -> b
coe Integer
v1))
T_K'38'__56
v2 T_Tree_166
v3 AgdaAny
v8 T__'8764'_'8852'__30
v5))
T_Fin_6
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_headTail_634 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_634 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T_Σ_14
d_headTail_634 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_166
v9
= Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 Integer
v8 T_Tree_166
v9
du_headTail_634 ::
Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_634 :: Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 Integer
v0 T_Tree_166
v1
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1 of
C_node_194 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_166
v6 T_Tree_166
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_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
-> 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_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 (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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v6 of
C_leaf_178 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_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
-> 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_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 (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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
(T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)))
T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
T_Tree_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_initLast_684 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_684 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T_Σ_14
d_initLast_684 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_166
v9
= Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 Integer
v8 T_Tree_166
v9
du_initLast_684 ::
Integer -> T_Tree_166 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_684 :: Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 Integer
v0 T_Tree_166
v1
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1 of
C_node_194 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_166
v6 T_Tree_166
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_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
-> 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_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v7 of
C_leaf_178 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_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_initLast_684 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
-> 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_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
T_Tree_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_join_740 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
T_Tree_166 ->
T_Tree_166 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join_740 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join_740 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
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_166
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
= T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_740 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_166
v12 T_Tree_166
v13 T__'8764'_'8852'__30
v14
du_join_740 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
Integer ->
Integer ->
T_Tree_166 ->
T_Tree_166 ->
MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join_740 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_740 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 Integer
v4 Integer
v5 Integer
v6 T_Tree_166
v7 T_Tree_166
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_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
-> 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_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (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_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v8 of
C_leaf_178 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_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Σ_14
du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v12) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
-> 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_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (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_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
du_cast'691'_302 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10)
d_empty_776 ::
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_166
d_empty_776 :: T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
d_empty_776 ~T_Value_38
v0 ~Maybe (Maybe AgdaAny)
v1 ~Maybe (Maybe AgdaAny)
v2 = T__'60''8314'__20 -> T_Tree_166
du_empty_776
du_empty_776 ::
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
T_Tree_166
du_empty_776 :: T__'60''8314'__20 -> T_Tree_166
du_empty_776 = (T__'60''8314'__20 -> T_Tree_166)
-> T__'60''8314'__20 -> T_Tree_166
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_166
C_leaf_178
d_singleton_784 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_166
d_singleton_784 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Tree_166
d_singleton_784 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
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_166
du_singleton_784 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
du_singleton_784 ::
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_166
du_singleton_784 :: AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166
du_singleton_784 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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_166
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 (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_166) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_166
C_leaf_178 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)) ((T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_166
C_leaf_178 (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_166
forall a. a
MAlonzo.RTE.mazUnreachableError
d_insertWith_804 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insertWith_804 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
d_insertWith_804 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
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_166
v11 T_Σ_14
v12
= T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_166
v11 T_Σ_14
v12
du_insertWith_804 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny ->
(Maybe AgdaAny -> AgdaAny) ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insertWith_804 :: T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_166
v4 T_Σ_14
v5
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v4 of
C_leaf_178 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_6 -> T_Fin_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_6 -> T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_suc_16
(T_Fin_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10))
((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166
du_singleton_784 (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_194 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_166
v10 T_Tree_166
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_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516
(T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
(T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
AgdaAny
v2 AgdaAny
v13 in
AgdaAny -> T_Σ_14
forall a b. a -> b
coe
(case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v18
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> 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_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_352 (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_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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'_158 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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10)
((Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 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_864 -> T_StrictPartialOrder_472)
-> AgdaAny -> t
forall a b. a -> b
coe
T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.du_strictPartialOrder_916
(T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) 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_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v21)))
AgdaAny
v2 AgdaAny
v13 AgdaAny
v19))
AgdaAny
v14)))))
T_Tree_166
v10 T_Tree_166
v11 T__'8764'_'8852'__30
v12)
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v20
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> 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_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_442 (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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v10)
((T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_136
_ -> 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_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_insert_906 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
AgdaAny ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insert_906 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
d_insert_906 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
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_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insert_906 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v9 AgdaAny
v10
du_insert_906 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny ->
AgdaAny ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insert_906 :: T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insert_906 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3
= (T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
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_922 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_delete_922 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
d_delete_922 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
= T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
du_delete_922 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_delete_922 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 T_StrictTotalOrder_864
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Integer
v3 AgdaAny
v4 T_Tree_166
v5 T_Σ_14
v6
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v5 of
C_leaf_178 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_6 -> AgdaAny
forall a b. a -> b
coe T_Fin_6
MAlonzo.Code.Data.Fin.Base.C_zero_10) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v5)
C_node_194 Integer
v7 Integer
v8 T_K'38'__56
v10 T_Tree_166
v11 T_Tree_166
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_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516
(T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
(T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
AgdaAny
v15 AgdaAny
v4 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v20
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> 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_166
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_580 (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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11)
((T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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'_158 AgdaAny
v21
-> (T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> 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_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_740 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v11) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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'_166 AgdaAny
v22
-> (Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_166
-> 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_166
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_518 (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_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v12) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
T_Tri_136
_ -> 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_166
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_lookup_1020 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
AgdaAny ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
d_lookup_1020 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> Maybe AgdaAny
d_lookup_1020 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
= T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v9 T_Tree_166
v10 T_Σ_14
v11
du_lookup_1020 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
AgdaAny ->
T_Tree_166 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 T_Tree_166
v3 T_Σ_14
v4
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
C_leaf_178 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_194 Integer
v5 Integer
v6 T_K'38'__56
v8 T_Tree_166
v9 T_Tree_166
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_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516
(T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
(T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))
AgdaAny
v12 AgdaAny
v2 in
AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v17
-> (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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 -> 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'_158 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
v2 AgdaAny
v18
AgdaAny
v13)
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v19
-> (T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1020 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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 (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_136
_ -> 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_166
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_foldr_1100 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.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_166 -> AgdaAny
d_foldr_1100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> 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_166
-> AgdaAny
d_foldr_1100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
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_166
v13
= (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 T_Tree_166
v13
du_foldr_1100 ::
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_166
v2
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v2 of
C_leaf_178 T__'60''8314'__20
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
C_node_194 Integer
v3 Integer
v4 T_K'38'__56
v6 T_Tree_166
v7 T_Tree_166
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_166 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 ((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_166 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
du_foldr_1100 ((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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v8)))
(T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)
T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_166
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toDiffList_1126 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) ->
Integer ->
T_Tree_166 ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toDiffList_1126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> [T_K'38'__56]
-> [T_K'38'__56]
d_toDiffList_1126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_166
v9
= T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 T_Tree_166
v9
du_toDiffList_1126 ::
T_Tree_166 ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
[MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toDiffList_1126 :: T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 T_Tree_166
v0
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v0 of
C_leaf_178 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_194 Integer
v1 Integer
v2 T_K'38'__56
v4 T_Tree_166
v5 T_Tree_166
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_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)))
T_Tree_166
_ -> [T_K'38'__56] -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toList_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_864 ->
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_166 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_1140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> [T_K'38'__56]
d_toList_1140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_166
v9
= T_Tree_166 -> [T_K'38'__56]
du_toList_1140 T_Tree_166
v9
du_toList_1140 ::
T_Tree_166 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_1140 :: T_Tree_166 -> [T_K'38'__56]
du_toList_1140 T_Tree_166
v0
= (T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> T_Tree_166 -> AgdaAny -> [T_K'38'__56]
forall a b. a -> b
coe
T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1126 T_Tree_166
v0
([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
d_size_1150 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
Maybe (Maybe AgdaAny) ->
Maybe (Maybe AgdaAny) -> Integer -> T_Tree_166 -> Integer
d_size_1150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> Integer
d_size_1150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 = T_Tree_166 -> Integer
du_size_1150
du_size_1150 :: T_Tree_166 -> Integer
du_size_1150 :: T_Tree_166 -> Integer
du_size_1150
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_166 -> Integer
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
(([AgdaAny] -> Integer) -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> Integer
MAlonzo.Code.Data.List.Base.du_length_296)
((T_Tree_166 -> [T_K'38'__56]) -> AgdaAny
forall a b. a -> b
coe T_Tree_166 -> [T_K'38'__56]
du_toList_1140)
d_Val_1164 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_1164 :: T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Val_1164 = T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_Wal_1166 ::
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
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_1166 :: T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Wal_1166 = T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
d_map_1174 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.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_166 -> T_Tree_166
d_map_1174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_166
-> T_Tree_166
d_map_1174 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_864
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_166
v12
= (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_166
v12
du_map_1174 ::
(AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_166
v1
= case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1 of
C_leaf_178 T__'60''8314'__20
v2 -> T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v1
C_node_194 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_166
v6 T_Tree_166
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_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_166
forall a b. a -> b
coe
Integer
-> Integer
-> T_K'38'__56
-> T_Tree_166
-> T_Tree_166
-> T__'8764'_'8852'__30
-> T_Tree_166
C_node_194 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_166 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6))
(((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
du_map_1174 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v7)) T__'8764'_'8852'__30
v8
T_K'38'__56
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Tree_166
_ -> T_Tree_166
forall a. a
MAlonzo.RTE.mazUnreachableError