{-# 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.Untyped.Equality 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.Bool
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Constant.AtomicType
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Bool.Properties
import qualified MAlonzo.Code.Data.Fin.Properties
import qualified MAlonzo.Code.Data.Integer.Properties
import qualified MAlonzo.Code.Data.List.Properties
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.String.Properties
import qualified MAlonzo.Code.Data.Unit.Properties
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Utils
data HasEq a = Eq a => HasEq
d_DecEq_6 :: p -> ()
d_DecEq_6 p
a0 = ()
newtype T_DecEq_6
= C_constructor_14 (AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20)
d__'8799'__12 ::
T_DecEq_6 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__12 :: T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__12 T_DecEq_6
v0
= case T_DecEq_6 -> T_DecEq_6
forall a b. a -> b
coe T_DecEq_6
v0 of
C_constructor_14 AgdaAny -> AgdaAny -> T_Dec_20
v1 -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1
T_DecEq_6
_ -> AgdaAny -> AgdaAny -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8799'__18 ::
T_DecEq_6 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__18 :: T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__18 T_DecEq_6
v0 = (T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)
type T_HasEq_20 a0 = HasEq a0
d_HasEq_20 :: a
d_HasEq_20
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Untyped.Equality.HasEq"
d_hasEq'45'TyTag_24 :: a
d_hasEq'45'TyTag_24
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Untyped.Equality.hasEq-TyTag"
d_HsEq_28 :: p -> ()
d_HsEq_28 p
a0 = ()
newtype T_HsEq_28 = C_constructor_36 (AgdaAny -> AgdaAny -> Bool)
d_hsEq_34 :: T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_34 :: T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_34 T_HsEq_28
v0
= case T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
v0 of
C_constructor_36 AgdaAny -> AgdaAny -> Bool
v1 -> (AgdaAny -> AgdaAny -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Bool
v1
T_HsEq_28
_ -> AgdaAny -> AgdaAny -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
d_hsEq_40 :: T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_40 :: T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_40 T_HsEq_28
v0 = (T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_34 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
v0)
d_eqArray_46 ::
forall xA.
() ->
T_HasEq_20 xA ->
MAlonzo.Code.Utils.T_Array_602 xA ->
MAlonzo.Code.Utils.T_Array_602 xA -> Bool
d_eqArray_46 :: forall xA.
() -> T_HasEq_20 xA -> T_Array_602 xA -> T_Array_602 xA -> Bool
d_eqArray_46 = \ ()
_ T_HasEq_20 xA
HasEq -> T_Array_602 xA -> T_Array_602 xA -> Bool
forall a. Eq a => a -> a -> Bool
(==)
d_decEq'45'TmCon_48 ::
MAlonzo.Code.RawU.T_TmCon_204 ->
MAlonzo.Code.RawU.T_TmCon_204 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decEq'45'TmCon_48 :: T_TmCon_204 -> T_TmCon_204 -> T_Dec_20
d_decEq'45'TmCon_48 T_TmCon_204
v0 T_TmCon_204
v1
= case T_TmCon_204 -> T_TmCon_204
forall a b. a -> b
coe T_TmCon_204
v0 of
MAlonzo.Code.RawU.C_tmCon_208 T__'8866''9839'_4
v2 AgdaAny
v3
-> case T_TmCon_204 -> T_TmCon_204
forall a b. a -> b
coe T_TmCon_204
v1 of
MAlonzo.Code.RawU.C_tmCon_208 T__'8866''9839'_4
v4 AgdaAny
v5
-> let v6 :: T_Dec_20
v6 = T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_20
MAlonzo.Code.RawU.d_decTyTag_70 (T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v2) (T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v4) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v6 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v7 T_Reflects_16
v8
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v7
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v8)
(let v9 :: AgdaAny
v9 = (T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20
d_decEq'45''10214'_'10215'tag_52 T__'8866''9839'_4
v2 AgdaAny
v3 AgdaAny
v5 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v10 T_Reflects_16
v11
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v10
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v11)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v11)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v10)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v8)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v7)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_TmCon_204
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
T_TmCon_204
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_decEq'45''10214'_'10215'tag_52 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decEq'45''10214'_'10215'tag_52 :: T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20
d_decEq'45''10214'_'10215'tag_52 T__'8866''9839'_4
v0
= case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v0 of
MAlonzo.Code.Builtin.Signature.C_'96'_8 T_Fin_10
v2
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe (\ AgdaAny
v3 AgdaAny
v4 -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v2
-> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v2 of
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aInteger_8
-> (Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Integer.Properties.d__'8799'__2800
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBytestring_10
-> (T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
d_HsEqBytestring_432)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aString_12
-> (T_String_6 -> T_String_6 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Dec_20
MAlonzo.Code.Data.String.Properties.d__'8799'__54
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 -> T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
MAlonzo.Code.Data.Unit.Properties.du__'8799'__8)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBool_16
-> (Bool -> Bool -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe Bool -> Bool -> T_Dec_20
MAlonzo.Code.Data.Bool.Properties.d__'8799'__3196
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18
-> (T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
d_HsEqDATA_464)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aValue_20
-> (T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
d_HsEqValue_466)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g1'45'element_22
-> (T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
d_HsEqBlsG1_458)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g2'45'element_24
-> (T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
d_HsEqBlsG2_460)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'mlresult_26
-> (T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
d_HsEqBlsMlResult_462)
T_AtomicTyCon_6
_ -> AgdaAny -> AgdaAny -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v2
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(\ AgdaAny
v3 ->
case AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v3 of
[AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_458
-> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v4 ->
case AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v4 of
[AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_458
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
MAlonzo.Code.Utils.C__'8759'__460 AgdaAny
v5 [AgdaAny]
v6
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Utils.C__'8759'__460 AgdaAny
v4 [AgdaAny]
v5
-> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v6 ->
case AgdaAny -> [AgdaAny]
forall a b. a -> b
coe AgdaAny
v6 of
[AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_458
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Utils.C__'8759'__460 AgdaAny
v7 [AgdaAny]
v8
-> let v9 :: AgdaAny
v9 = (T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20
d_decEq'45''10214'_'10215'tag_52 T__'8866''9839'_4
v2 AgdaAny
v4 AgdaAny
v7 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v10 T_Reflects_16
v11
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v10
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v11)
(let v12 :: AgdaAny
v12
= (T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> [AgdaAny] -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20
d_decEq'45''10214'_'10215'tag_52
((T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe
T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_list_16
T__'8866''9839'_4
v2)
[AgdaAny]
v5 [AgdaAny]
v8 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v12 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v13 T_Reflects_16
v14
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v13
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v14)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v13)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v14)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v13)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v11)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v10)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Builtin.Signature.C_array_20 T__'8866''9839'_4
v2
-> (T_Array_602 AgdaAny -> T_Array_602 AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe T_Array_602 AgdaAny -> T_Array_602 AgdaAny -> T_Dec_20
du_decEq'45'Array'45''10214'_'10215'tag_536
MAlonzo.Code.Builtin.Signature.C_pair_24 T__'8866''9839'_4
v2 T__'8866''9839'_4
v3
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(\ AgdaAny
v4 ->
case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v4 of
MAlonzo.Code.Utils.C__'44'__450 AgdaAny
v5 AgdaAny
v6
-> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v7 ->
case AgdaAny -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Utils.C__'44'__450 AgdaAny
v8 AgdaAny
v9
-> let v10 :: AgdaAny
v10
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84
((T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20
d_decEq'45''10214'_'10215'tag_52 T__'8866''9839'_4
v2 AgdaAny
v5 AgdaAny
v8)
((T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20
d_decEq'45''10214'_'10215'tag_52 T__'8866''9839'_4
v3 AgdaAny
v6 AgdaAny
v9) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v10 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v12 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v13
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
(AgdaAny, AgdaAny)
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
(AgdaAny, AgdaAny)
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866''9839'_4
_ -> AgdaAny -> AgdaAny -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_decEq'45''8866'_56 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decEq'45''8866'_56 :: Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2
= case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v3
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v4
-> let v5 :: AgdaAny
v5
= (T_Fin_10 -> T_Fin_10 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Fin_10 -> T_Fin_10 -> T_Dec_20
MAlonzo.Code.Data.Fin.Properties.du__'8799'__50 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v3)
(T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v4) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v5 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v3
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> let v5 :: T_Dec_20
v5
= Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56
((Integer -> Integer -> Integer) -> AgdaAny -> AgdaAny -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0)) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v5 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v3 T__'8866'_14
v4
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v5 T__'8866'_14
v6
-> let v7 :: T_Dec_20
v7 = Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(let v8 :: T_Dec_20
v8 = Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v3
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> let v5 :: T_Dec_20
v5 = Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v5 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v3
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> let v5 :: T_Dec_20
v5 = Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v5 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v3
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v4
-> let v5 :: T_Dec_20
v5 = T_TmCon_204 -> T_TmCon_204 -> T_Dec_20
d_decEq'45'TmCon_48 (T_TmCon_204 -> T_TmCon_204
forall a b. a -> b
coe T_TmCon_204
v3) (T_TmCon_204 -> T_TmCon_204
forall a b. a -> b
coe T_TmCon_204
v4) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v5 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_constr_34 Integer
v3 [T__'8866'_14]
v4
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v5 T__'8866'_14
v6
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v5 [T__'8866'_14]
v6
-> let v7 :: AgdaAny
v7
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
AgdaAny
forall a. a
erased
(\ AgdaAny
v7 ->
(Integer -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> AgdaAny
MAlonzo.Code.Data.Nat.Properties.du_'8801''8658''8801''7495'_2786
(Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3))
((Bool -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_72
((Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Bool
eqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5))) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(let v8 :: T_Dec_20
v8 = Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20
d_decEqList'45''8866'_60 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) ([T__'8866'_14] -> [T__'8866'_14]
forall a b. a -> b
coe [T__'8866'_14]
v4) ([T__'8866'_14] -> [T__'8866'_14]
forall a b. a -> b
coe [T__'8866'_14]
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v3 [T__'8866'_14]
v4
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v5 T__'8866'_14
v6
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v5 [T__'8866'_14]
v6
-> let v7 :: T_Dec_20
v7 = Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(let v8 :: T_Dec_20
v8 = Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20
d_decEqList'45''8866'_60 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) ([T__'8866'_14] -> [T__'8866'_14]
forall a b. a -> b
coe [T__'8866'_14]
v4) ([T__'8866'_14] -> [T__'8866'_14]
forall a b. a -> b
coe [T__'8866'_14]
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v3
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> let v5 :: AgdaAny
v5
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
AgdaAny
forall a. a
erased
(\ AgdaAny
v5 ->
(Integer -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> AgdaAny
MAlonzo.Code.Data.Nat.Properties.du_'8801''8658''8801''7495'_2786
((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_enumBuiltin_454 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v3)))
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
((Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> Bool
eqInt ((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_enumBuiltin_454 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v3))
((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_enumBuiltin_454 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v4)))
((Bool -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_70
((Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> Bool
eqInt ((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_enumBuiltin_454 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v3))
((T_Builtin_2 -> Integer) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> Integer
MAlonzo.Code.Builtin.d_enumBuiltin_454 (T_Builtin_2 -> AgdaAny
forall a b. a -> b
coe T_Builtin_2
v4))))) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v5 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v6 T_Reflects_16
v7
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v6
then let v8 :: AgdaAny
v8
= AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
else (let v8 :: AgdaAny
v8
= AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v7)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v3
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v3
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v3 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v3
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v3
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_204
v3
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v3 [T__'8866'_14]
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v3 [T__'8866'_14]
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v3
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_decEqList'45''8866'_60 ::
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decEqList'45''8866'_60 :: Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20
d_decEqList'45''8866'_60 Integer
v0 [T__'8866'_14]
v1 [T__'8866'_14]
v2
= case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
[]
-> case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v2 of
[]
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
(:) AgdaAny
v3 [AgdaAny]
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
(:) AgdaAny
v3 [AgdaAny]
v4
-> case [T__'8866'_14] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866'_14]
v2 of
[]
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
(:) AgdaAny
v5 [AgdaAny]
v6
-> let v7 :: T_Dec_20
v7 = Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (AgdaAny -> T__'8866'_14
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> T__'8866'_14
forall a b. a -> b
coe AgdaAny
v5) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(let v8 :: T_Dec_20
v8 = Integer -> [T__'8866'_14] -> [T__'8866'_14] -> T_Dec_20
d_decEqList'45''8866'_60 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) ([AgdaAny] -> [T__'8866'_14]
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> [T__'8866'_14]
forall a b. a -> b
coe [AgdaAny]
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_decPointwise_72 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
[AgdaAny] ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decPointwise_72 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
d_decPointwise_72 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 [AgdaAny]
v6 [AgdaAny]
v7
= (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_decPointwise_72 AgdaAny -> AgdaAny -> T_Dec_20
v5 [AgdaAny]
v6 [AgdaAny]
v7
du_decPointwise_72 ::
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
[AgdaAny] ->
[AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_decPointwise_72 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_decPointwise_72 AgdaAny -> AgdaAny -> T_Dec_20
v0 [AgdaAny]
v1 [AgdaAny]
v2
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
[]
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
[]
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe
T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56))
(:) AgdaAny
v3 [AgdaAny]
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
(:) AgdaAny
v3 [AgdaAny]
v4
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
[]
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
(:) AgdaAny
v5 [AgdaAny]
v6
-> let v7 :: AgdaAny
v7 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v3 AgdaAny
v5 in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(let v8 :: AgdaAny
v8 = ((AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_decPointwise_72 ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v10 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v11
-> case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v12 T_Reflects_16
v13
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v12
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v13 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v14
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v12)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
AgdaAny
v11 AgdaAny
v14))
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v13)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v12)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_DecAtomicTyCon_148 :: T_DecEq_6
d_DecAtomicTyCon_148 :: T_DecEq_6
d_DecAtomicTyCon_148
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
((T_AtomicTyCon_6 -> T_AtomicTyCon_6 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_AtomicTyCon_6 -> T_AtomicTyCon_6 -> T_Dec_20
MAlonzo.Code.Builtin.Constant.AtomicType.d_decAtomicTyCon_28)
d_DecEq'45'TmCon_150 :: T_DecEq_6
d_DecEq'45'TmCon_150 :: T_DecEq_6
d_DecEq'45'TmCon_150
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14 ((T_TmCon_204 -> T_TmCon_204 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_TmCon_204 -> T_TmCon_204 -> T_Dec_20
d_decEq'45'TmCon_48)
d_DecEq'45''8866'_154 :: Integer -> T_DecEq_6
d_DecEq'45''8866'_154 :: Integer -> T_DecEq_6
d_DecEq'45''8866'_154 Integer
v0
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14 ((Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_decEq'45''8866'_56 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0))
d_DecEq'45'List_160 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'List_160 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'List_160 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List_160 T_DecEq_6
v1
du_DecEq'45'List_160 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List_160 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List_160 T_DecEq_6
v0
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
(((AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Properties.du_'8801''45'dec_60
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)))
d_DecEq'45'Builtin_164 :: T_DecEq_6
d_DecEq'45'Builtin_164 :: T_DecEq_6
d_DecEq'45'Builtin_164
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14 ((T_Builtin_2 -> T_Builtin_2 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> T_Builtin_2 -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_468)
d_DecEq'45'ℕ_166 :: T_DecEq_6
d_DecEq'45'ℕ_166 :: T_DecEq_6
d_DecEq'45'ℕ_166
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
((Integer -> Integer -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2796)
d_DecEq'45'ℤ_168 :: T_DecEq_6
d_DecEq'45'ℤ_168 :: T_DecEq_6
d_DecEq'45'ℤ_168
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
((Integer -> Integer -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Integer.Properties.d__'8799'__2800)
d_DecEq'45'Fin_172 :: Integer -> T_DecEq_6
d_DecEq'45'Fin_172 :: Integer -> T_DecEq_6
d_DecEq'45'Fin_172 ~Integer
v0 = T_DecEq_6
du_DecEq'45'Fin_172
du_DecEq'45'Fin_172 :: T_DecEq_6
du_DecEq'45'Fin_172 :: T_DecEq_6
du_DecEq'45'Fin_172
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
((T_Fin_10 -> T_Fin_10 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_Fin_10 -> T_Fin_10 -> T_Dec_20
MAlonzo.Code.Data.Fin.Properties.du__'8799'__50)
d_DecEq'45'String_174 :: T_DecEq_6
d_DecEq'45'String_174 :: T_DecEq_6
d_DecEq'45'String_174
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
((T_String_6 -> T_String_6 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Dec_20
MAlonzo.Code.Data.String.Properties.d__'8799'__54)
d_DecEq'45'Unit_176 :: T_DecEq_6
d_DecEq'45'Unit_176 :: T_DecEq_6
d_DecEq'45'Unit_176
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
(\ AgdaAny
v0 AgdaAny
v1 -> T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
MAlonzo.Code.Data.Unit.Properties.du__'8799'__8)
d_DecEq'45'Bool_178 :: T_DecEq_6
d_DecEq'45'Bool_178 :: T_DecEq_6
d_DecEq'45'Bool_178
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
((Bool -> Bool -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe Bool -> Bool -> T_Dec_20
MAlonzo.Code.Data.Bool.Properties.d__'8799'__3196)
d_DecEq'45'TyTag_180 :: T_DecEq_6
d_DecEq'45'TyTag_180 :: T_DecEq_6
d_DecEq'45'TyTag_180
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14 ((T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_20
MAlonzo.Code.RawU.d_decTyTag_70)
d_DecEq'45''10214'_'10215'tag_184 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 -> T_DecEq_6
d_DecEq'45''10214'_'10215'tag_184 :: T__'8866''9839'_4 -> T_DecEq_6
d_DecEq'45''10214'_'10215'tag_184 T__'8866''9839'_4
v0
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14 ((T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_20
d_decEq'45''10214'_'10215'tag_52 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v0))
d_listDec_190 ::
() ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Utils.T_List_454 AgdaAny ->
MAlonzo.Code.Utils.T_List_454 AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_listDec_190 :: ()
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
d_listDec_190 ~()
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 [AgdaAny]
v2 [AgdaAny]
v3 = (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_listDec_190 AgdaAny -> AgdaAny -> T_Dec_20
v1 [AgdaAny]
v2 [AgdaAny]
v3
du_listDec_190 ::
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Utils.T_List_454 AgdaAny ->
MAlonzo.Code.Utils.T_List_454 AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_listDec_190 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_listDec_190 AgdaAny -> AgdaAny -> T_Dec_20
v0 [AgdaAny]
v1 [AgdaAny]
v2
= case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
[AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_458
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
[AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_458
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
MAlonzo.Code.Utils.C__'8759'__460 AgdaAny
v3 [AgdaAny]
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Utils.C__'8759'__460 AgdaAny
v3 [AgdaAny]
v4
-> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
[AgdaAny]
MAlonzo.Code.Utils.C_'91''93'_458
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Utils.C__'8759'__460 AgdaAny
v5 [AgdaAny]
v6
-> let v7 :: AgdaAny
v7 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v3 AgdaAny
v5 in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v8 T_Reflects_16
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v9)
(let v10 :: AgdaAny
v10 = ((AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_listDec_190 ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v10 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v9)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
[AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_pairDec_278 ::
() ->
() ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Utils.T__'215'__436 AgdaAny AgdaAny ->
MAlonzo.Code.Utils.T__'215'__436 AgdaAny AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_pairDec_278 :: ()
-> ()
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny, AgdaAny)
-> (AgdaAny, AgdaAny)
-> T_Dec_20
d_pairDec_278 ~()
v0 ~()
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2 AgdaAny -> AgdaAny -> T_Dec_20
v3 (AgdaAny, AgdaAny)
v4 (AgdaAny, AgdaAny)
v5 = (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny, AgdaAny)
-> (AgdaAny, AgdaAny)
-> T_Dec_20
du_pairDec_278 AgdaAny -> AgdaAny -> T_Dec_20
v2 AgdaAny -> AgdaAny -> T_Dec_20
v3 (AgdaAny, AgdaAny)
v4 (AgdaAny, AgdaAny)
v5
du_pairDec_278 ::
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Utils.T__'215'__436 AgdaAny AgdaAny ->
MAlonzo.Code.Utils.T__'215'__436 AgdaAny AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_pairDec_278 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny, AgdaAny)
-> (AgdaAny, AgdaAny)
-> T_Dec_20
du_pairDec_278 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 (AgdaAny, AgdaAny)
v2 (AgdaAny, AgdaAny)
v3
= case (AgdaAny, AgdaAny) -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe (AgdaAny, AgdaAny)
v2 of
MAlonzo.Code.Utils.C__'44'__450 AgdaAny
v4 AgdaAny
v5
-> case (AgdaAny, AgdaAny) -> (AgdaAny, AgdaAny)
forall a b. a -> b
coe (AgdaAny, AgdaAny)
v3 of
MAlonzo.Code.Utils.C__'44'__450 AgdaAny
v6 AgdaAny
v7
-> let v8 :: AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v4 AgdaAny
v6 in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(let v9 :: AgdaAny
v9 = (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v5 AgdaAny
v7 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(let v10 :: AgdaAny
v10
= case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v10 T_Reflects_16
v11
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v10)
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v11)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> let v13 :: AgdaAny
v13
= case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v13 T_Reflects_16
v14
-> case Bool -> Bool
forall a b. a -> b
coe Bool
v13 of
Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8
-> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v14 of
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v13)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T_Reflects_16
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10
Bool
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v12 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v14
-> case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v15 T_Reflects_16
v16
-> case Bool -> Bool
forall a b. a -> b
coe Bool
v15 of
Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
-> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v16 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v17
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v15)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
AgdaAny
forall a. a
erased)
T_Reflects_16
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13
Bool
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13
else (case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v12 of
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T_Reflects_16
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)))
(AgdaAny, AgdaAny)
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
(AgdaAny, AgdaAny)
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_DecEq'45'UList_404 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'UList_404 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'UList_404 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T_DecEq_6
du_DecEq'45'UList_404 T_DecEq_6
v1
du_DecEq'45'UList_404 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'UList_404 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'UList_404 T_DecEq_6
v0
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14 (((AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
du_listDec_190 ((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)))
d_DecEq'45'Pair_416 ::
() -> () -> T_DecEq_6 -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'Pair_416 :: () -> () -> T_DecEq_6 -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'Pair_416 ~()
v0 ~()
v1 T_DecEq_6
v2 T_DecEq_6
v3 = T_DecEq_6 -> T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Pair_416 T_DecEq_6
v2 T_DecEq_6
v3
du_DecEq'45'Pair_416 :: T_DecEq_6 -> T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Pair_416 :: T_DecEq_6 -> T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Pair_416 T_DecEq_6
v0 T_DecEq_6
v1
= ((AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20) -> T_DecEq_6
C_constructor_14
(((AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny, AgdaAny)
-> (AgdaAny, AgdaAny)
-> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny, AgdaAny)
-> (AgdaAny, AgdaAny)
-> T_Dec_20
du_pairDec_278 ((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0))
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v1)))
d_fromDec_426 :: () -> T_DecEq_6 -> T_HsEq_28
d_fromDec_426 :: () -> T_DecEq_6 -> T_HsEq_28
d_fromDec_426 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T_HsEq_28
du_fromDec_426 T_DecEq_6
v1
du_fromDec_426 :: T_DecEq_6 -> T_HsEq_28
du_fromDec_426 :: T_DecEq_6 -> T_HsEq_28
du_fromDec_426 T_DecEq_6
v0
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v1 AgdaAny
v2 ->
(T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_isYes_132
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecEq_6 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
d__'8799'__12 T_DecEq_6
v0 AgdaAny
v1 AgdaAny
v2)))
d_HsEqBytestring_432 :: T_HsEq_28
d_HsEqBytestring_432 :: T_HsEq_28
d_HsEqBytestring_432
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36 ((T_ByteString_426 -> T_ByteString_426 -> Bool) -> AgdaAny
forall a b. a -> b
coe T_ByteString_426 -> T_ByteString_426 -> Bool
MAlonzo.Code.Utils.d_eqByteString_430)
d_HsEqArray_438 :: () -> T_HasEq_20 AgdaAny -> T_HsEq_28
d_HsEqArray_438 :: () -> T_HasEq_20 AgdaAny -> T_HsEq_28
d_HsEqArray_438 ~()
v0 ~T_HasEq_20 AgdaAny
v1 = T_HsEq_28
du_HsEqArray_438
du_HsEqArray_438 :: T_HsEq_28
du_HsEqArray_438 :: T_HsEq_28
du_HsEqArray_438
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36
((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 -> Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
d_HsEqList_446 :: () -> T_DecEq_6 -> T_HsEq_28
d_HsEqList_446 :: () -> T_DecEq_6 -> T_HsEq_28
d_HsEqList_446 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T_HsEq_28
du_HsEqList_446 T_DecEq_6
v1
du_HsEqList_446 :: T_DecEq_6 -> T_HsEq_28
du_HsEqList_446 :: T_DecEq_6 -> T_HsEq_28
du_HsEqList_446 T_DecEq_6
v0
= (T_DecEq_6 -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe T_DecEq_6 -> T_HsEq_28
du_fromDec_426 ((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T_DecEq_6
du_DecEq'45'UList_404 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0))
d_HsEqPair_456 :: () -> () -> T_DecEq_6 -> T_DecEq_6 -> T_HsEq_28
d_HsEqPair_456 :: () -> () -> T_DecEq_6 -> T_DecEq_6 -> T_HsEq_28
d_HsEqPair_456 ~()
v0 ~()
v1 T_DecEq_6
v2 T_DecEq_6
v3 = T_DecEq_6 -> T_DecEq_6 -> T_HsEq_28
du_HsEqPair_456 T_DecEq_6
v2 T_DecEq_6
v3
du_HsEqPair_456 :: T_DecEq_6 -> T_DecEq_6 -> T_HsEq_28
du_HsEqPair_456 :: T_DecEq_6 -> T_DecEq_6 -> T_HsEq_28
du_HsEqPair_456 T_DecEq_6
v0 T_DecEq_6
v1
= (T_DecEq_6 -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe T_DecEq_6 -> T_HsEq_28
du_fromDec_426 ((T_DecEq_6 -> T_DecEq_6 -> T_DecEq_6)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Pair_416 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v1))
d_HsEqBlsG1_458 :: T_HsEq_28
d_HsEqBlsG1_458 :: T_HsEq_28
d_HsEqBlsG1_458
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36
((T_Bls12'45'381'45'G1'45'Element_764
-> T_Bls12'45'381'45'G1'45'Element_764 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'G1'45'Element_764
-> T_Bls12'45'381'45'G1'45'Element_764 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'G1'45'Element_766)
d_HsEqBlsG2_460 :: T_HsEq_28
d_HsEqBlsG2_460 :: T_HsEq_28
d_HsEqBlsG2_460
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36
((T_Bls12'45'381'45'G2'45'Element_768
-> T_Bls12'45'381'45'G2'45'Element_768 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'G2'45'Element_768
-> T_Bls12'45'381'45'G2'45'Element_768 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'G2'45'Element_770)
d_HsEqBlsMlResult_462 :: T_HsEq_28
d_HsEqBlsMlResult_462 :: T_HsEq_28
d_HsEqBlsMlResult_462
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36
((T_Bls12'45'381'45'MlResult_772
-> T_Bls12'45'381'45'MlResult_772 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'MlResult_772
-> T_Bls12'45'381'45'MlResult_772 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'MlResult_774)
d_HsEqDATA_464 :: T_HsEq_28
d_HsEqDATA_464 :: T_HsEq_28
d_HsEqDATA_464
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36 ((T_DATA_618 -> T_DATA_618 -> Bool) -> AgdaAny
forall a b. a -> b
coe T_DATA_618 -> T_DATA_618 -> Bool
MAlonzo.Code.Utils.d_eqDATA_630)
d_HsEqValue_466 :: T_HsEq_28
d_HsEqValue_466 :: T_HsEq_28
d_HsEqValue_466
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> Bool) -> T_HsEq_28
C_constructor_36 ((T_Value_776 -> T_Value_776 -> Bool) -> AgdaAny
forall a b. a -> b
coe T_Value_776 -> T_Value_776 -> Bool
MAlonzo.Code.Utils.d_eqValue_778)
d_HsEq'45''10214'_'10215'tag_470 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 -> T_HsEq_28
d_HsEq'45''10214'_'10215'tag_470 :: T__'8866''9839'_4 -> T_HsEq_28
d_HsEq'45''10214'_'10215'tag_470 T__'8866''9839'_4
v0
= case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v0 of
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v2
-> case T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v2 of
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aInteger_8
-> (T_DecEq_6 -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe T_DecEq_6 -> T_HsEq_28
du_fromDec_426 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
d_DecEq'45'ℤ_168)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBytestring_10
-> T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
d_HsEqBytestring_432
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aString_12
-> (T_DecEq_6 -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe T_DecEq_6 -> T_HsEq_28
du_fromDec_426 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
d_DecEq'45'String_174)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14
-> (T_DecEq_6 -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe T_DecEq_6 -> T_HsEq_28
du_fromDec_426 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
d_DecEq'45'Unit_176)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBool_16
-> (T_DecEq_6 -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe T_DecEq_6 -> T_HsEq_28
du_fromDec_426 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
d_DecEq'45'Bool_178)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18
-> T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
d_HsEqDATA_464
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aValue_20
-> T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
d_HsEqValue_466
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g1'45'element_22
-> T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
d_HsEqBlsG1_458
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g2'45'element_24
-> T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
d_HsEqBlsG2_460
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'mlresult_26
-> T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
d_HsEqBlsMlResult_462
T_AtomicTyCon_6
_ -> T_HsEq_28
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v2
-> (T_DecEq_6 -> T_HsEq_28) -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe
T_DecEq_6 -> T_HsEq_28
du_HsEqList_446 ((T__'8866''9839'_4 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> T_DecEq_6
d_DecEq'45''10214'_'10215'tag_184 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v2))
MAlonzo.Code.Builtin.Signature.C_array_20 T__'8866''9839'_4
v2
-> T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
du_HsEqArray_438
MAlonzo.Code.Builtin.Signature.C_pair_24 T__'8866''9839'_4
v2 T__'8866''9839'_4
v3
-> (T_DecEq_6 -> T_DecEq_6 -> T_HsEq_28)
-> AgdaAny -> AgdaAny -> T_HsEq_28
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6 -> T_HsEq_28
du_HsEqPair_456 ((T__'8866''9839'_4 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> T_DecEq_6
d_DecEq'45''10214'_'10215'tag_184 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v2))
((T__'8866''9839'_4 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> T_DecEq_6
d_DecEq'45''10214'_'10215'tag_184 (T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4
v3))
T__'8866''9839'_4
_ -> T_HsEq_28
forall a. a
MAlonzo.RTE.mazUnreachableError
d_magicNeg_486 :: a
d_magicNeg_486
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: Untyped.Equality.magicNeg"
d_builtinEq_492 ::
() ->
T_HsEq_28 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_builtinEq_492 :: () -> T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
d_builtinEq_492 ~()
v0 T_HsEq_28
v1 AgdaAny
v2 AgdaAny
v3 = T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 T_HsEq_28
v1 AgdaAny
v2 AgdaAny
v3
du_builtinEq_492 ::
T_HsEq_28 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_builtinEq_492 :: T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 T_HsEq_28
v0 AgdaAny
v1 AgdaAny
v2
= let v3 :: AgdaAny
v3 = (T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool)
-> T_HsEq_28 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_34 T_HsEq_28
v0 AgdaAny
v1 AgdaAny
v2 in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(if AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny
v3
then (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
else (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
d_hsEqArrayHelper_530 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 -> T_HsEq_28
d_hsEqArrayHelper_530 :: T__'8866''9839'_4 -> T_HsEq_28
d_hsEqArrayHelper_530 ~T__'8866''9839'_4
v0 = T_HsEq_28
du_hsEqArrayHelper_530
du_hsEqArrayHelper_530 :: T_HsEq_28
du_hsEqArrayHelper_530 :: T_HsEq_28
du_hsEqArrayHelper_530 = T_HsEq_28 -> T_HsEq_28
forall a b. a -> b
coe T_HsEq_28
du_HsEqArray_438
d_decEq'45'Array'45''10214'_'10215'tag_536 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Utils.T_Array_602 AgdaAny ->
MAlonzo.Code.Utils.T_Array_602 AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decEq'45'Array'45''10214'_'10215'tag_536 :: T__'8866''9839'_4
-> T_Array_602 AgdaAny -> T_Array_602 AgdaAny -> T_Dec_20
d_decEq'45'Array'45''10214'_'10215'tag_536 ~T__'8866''9839'_4
v0
= T_Array_602 AgdaAny -> T_Array_602 AgdaAny -> T_Dec_20
du_decEq'45'Array'45''10214'_'10215'tag_536
du_decEq'45'Array'45''10214'_'10215'tag_536 ::
MAlonzo.Code.Utils.T_Array_602 AgdaAny ->
MAlonzo.Code.Utils.T_Array_602 AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_decEq'45'Array'45''10214'_'10215'tag_536 :: T_Array_602 AgdaAny -> T_Array_602 AgdaAny -> T_Dec_20
du_decEq'45'Array'45''10214'_'10215'tag_536
= (T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> T_Array_602 AgdaAny
-> T_Array_602 AgdaAny
-> T_Dec_20
forall a b. a -> b
coe T_HsEq_28 -> AgdaAny -> AgdaAny -> T_Dec_20
du_builtinEq_492 (T_HsEq_28 -> AgdaAny
forall a b. a -> b
coe T_HsEq_28
du_hsEqArrayHelper_530)