{-# 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.VerifiedCompilation.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.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
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.Empty
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.Maybe.Properties
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
import qualified MAlonzo.Code.Relation.Nullary.Product
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Utils
d_DecEq_6 :: p -> ()
d_DecEq_6 p
a0 = ()
newtype T_DecEq_6
= C_DecEq'46'constructor_11 (AgdaAny ->
AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32)
d__'8799'__12 ::
T_DecEq_6 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__12 :: T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
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_DecEq'46'constructor_11 AgdaAny -> AgdaAny -> T_Dec_32
v1 -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v1
T_DecEq_6
_ -> AgdaAny -> AgdaAny -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8799'__16 ::
T_DecEq_6 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8799'__16 :: T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__16 T_DecEq_6
v0 = (T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)
d_decEq'45'TmCon_18 ::
MAlonzo.Code.RawU.T_TmCon_198 ->
MAlonzo.Code.RawU.T_TmCon_198 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_decEq'45'TmCon_18 :: T_TmCon_198 -> T_TmCon_198 -> T_Dec_32
d_decEq'45'TmCon_18 T_TmCon_198
v0 T_TmCon_198
v1
= case T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v0 of
MAlonzo.Code.RawU.C_tmCon_202 T__'8866''9839'_4
v2 AgdaAny
v3
-> case T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v1 of
MAlonzo.Code.RawU.C_tmCon_202 T__'8866''9839'_4
v4 AgdaAny
v5
-> let v6 :: T_Dec_32
v6 = T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_32
d_decEq'45'TyTag_20 (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_32
forall a b. a -> b
coe
(case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v6 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v7 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v8)
(let v9 :: t
v9 = (T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32
d_decEq'45''10214'_'10215'tag_24 T__'8866''9839'_4
v2 AgdaAny
v3 AgdaAny
v5 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v9 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v10 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v11)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v10)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v11)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v10)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v8)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v7)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_TmCon_198
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
T_TmCon_198
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_decEq'45'TyTag_20 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_decEq'45'TyTag_20 :: T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_32
d_decEq'45'TyTag_20 T__'8866''9839'_4
v0 T__'8866''9839'_4
v1
= 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
v3
-> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v1 of
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v5
-> let v6 :: T_Dec_32
v6
= T_AtomicTyCon_6 -> T_AtomicTyCon_6 -> T_Dec_32
MAlonzo.Code.Builtin.Constant.AtomicType.d_decAtomicTyCon_26
(T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v3) (T_AtomicTyCon_6 -> T_AtomicTyCon_6
forall a b. a -> b
coe T_AtomicTyCon_6
v5) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v6 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v7 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v8)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v7)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v8)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v7)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Builtin.Signature.C_pair_20 T__'8866''9839'_4
v5 T__'8866''9839'_4
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866''9839'_4
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v3
-> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v1 of
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v5
-> let v6 :: T_Dec_32
v6 = T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_32
d_decEq'45'TyTag_20 (T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v3) (T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v5) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v6 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v7 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v8)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v7)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v8)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v7)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Builtin.Signature.C_pair_20 T__'8866''9839'_4
v5 T__'8866''9839'_4
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866''9839'_4
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Builtin.Signature.C_pair_20 T__'8866''9839'_4
v3 T__'8866''9839'_4
v4
-> case T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe T__'8866''9839'_4
v1 of
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Builtin.Signature.C_pair_20 T__'8866''9839'_4
v6 T__'8866''9839'_4
v7
-> let v8 :: t
v8
= (T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecEq_6 -> T__'8866''9839'_4 -> T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 T_DecEq_6
d_DecEq'45'TyTag_152 T__'8866''9839'_4
v3 T__'8866''9839'_4
v6)
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecEq_6 -> T__'8866''9839'_4 -> T__'8866''9839'_4 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 T_DecEq_6
d_DecEq'45'TyTag_152 T__'8866''9839'_4
v4 T__'8866''9839'_4
v7) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v9 T_Reflects_14
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v10 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v11
-> (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
v11)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
AgdaAny
forall a. a
erased))
T_Reflects_14
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v10)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866''9839'_4
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866''9839'_4
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_decEq'45''10214'_'10215'tag_24 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_decEq'45''10214'_'10215'tag_24 :: T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32
d_decEq'45''10214'_'10215'tag_24 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_6
v2
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
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_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Integer.Properties.d__'8799'__1540
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBytestring_10
-> (T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32
du_builtinEq_292
(((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_ByteString_356 -> T_ByteString_356 -> Bool) -> AgdaAny
forall a b. a -> b
coe T_ByteString_356 -> T_ByteString_356 -> Bool
MAlonzo.Code.Utils.d_eqByteString_358))
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aString_12
-> (T_String_6 -> T_String_6 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe T_String_6 -> T_String_6 -> T_Dec_32
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_32
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 -> T_Dec_32 -> AgdaAny
forall a b. a -> b
coe T_Dec_32
MAlonzo.Code.Data.Unit.Properties.du__'8799'__8)
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBool_16
-> (Bool -> Bool -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe Bool -> Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d__'8799'__1510
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(\ AgdaAny
v3 AgdaAny
v4 ->
(Bool -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Dec_32
du_magicBoolDec_286 ((T_DATA_450 -> T_DATA_450 -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DATA_450 -> T_DATA_450 -> Bool
MAlonzo.Code.Utils.d_eqDATA_462 AgdaAny
v3 AgdaAny
v4))
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g1'45'element_20
-> (T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32
du_builtinEq_292
(((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_Bls12'45'381'45'G1'45'Element_464
-> T_Bls12'45'381'45'G1'45'Element_464 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'G1'45'Element_464
-> T_Bls12'45'381'45'G1'45'Element_464 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'G1'45'Element_466))
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g2'45'element_22
-> (T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32
du_builtinEq_292
(((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_Bls12'45'381'45'G2'45'Element_468
-> T_Bls12'45'381'45'G2'45'Element_468 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'G2'45'Element_468
-> T_Bls12'45'381'45'G2'45'Element_468 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'G2'45'Element_470))
T_AtomicTyCon_6
MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'mlresult_24
-> (T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32
du_builtinEq_292
(((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_Bls12'45'381'45'MlResult_472
-> T_Bls12'45'381'45'MlResult_472 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'MlResult_472
-> T_Bls12'45'381'45'MlResult_472 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'MlResult_474))
T_AtomicTyCon_6
_ -> AgdaAny -> AgdaAny -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Builtin.Signature.C_list_16 T__'8866''9839'_4
v2
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
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'_386
-> (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'_386
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
forall a. a
erased)
MAlonzo.Code.Utils.C__'8759'__388 AgdaAny
v5 [AgdaAny]
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
[AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Utils.C__'8759'__388 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'_386
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Utils.C__'8759'__388 AgdaAny
v7 [AgdaAny]
v8
-> let v9 :: t
v9 = (T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32
d_decEq'45''10214'_'10215'tag_24 T__'8866''9839'_4
v2 AgdaAny
v4 AgdaAny
v7 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v9 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v10 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v11)
(let v12 :: t
v12
= (T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> [AgdaAny] -> [AgdaAny] -> t
forall a b. a -> b
coe
T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32
d_decEq'45''10214'_'10215'tag_24
((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_32
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v13 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v14)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v13)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v14)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v13)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v11)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v10)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> 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_pair_20 T__'8866''9839'_4
v2 T__'8866''9839'_4
v3
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
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'__378 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'__378 AgdaAny
v8 AgdaAny
v9
-> let v10 :: t
v10
= (T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
((T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32
d_decEq'45''10214'_'10215'tag_24 T__'8866''9839'_4
v2 AgdaAny
v5 AgdaAny
v8)
((T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> AgdaAny -> AgdaAny -> T_Dec_32
d_decEq'45''10214'_'10215'tag_24 T__'8866''9839'_4
v3 AgdaAny
v6 AgdaAny
v9) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v11 T_Reflects_14
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v12 of
MAlonzo.Code.Relation.Nullary.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_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
AgdaAny
forall a. a
erased))
T_Reflects_14
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v12)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v11)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> 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_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_decPointwise_36 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_decPointwise_36 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
d_decPointwise_36 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 AgdaAny -> AgdaAny -> T_Dec_32
v5 [AgdaAny]
v6 [AgdaAny]
v7
= (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32
du_decPointwise_36 AgdaAny -> AgdaAny -> T_Dec_32
v5 [AgdaAny]
v6 [AgdaAny]
v7
du_decPointwise_36 ::
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
[AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_decPointwise_36 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32
du_decPointwise_36 AgdaAny -> AgdaAny -> T_Dec_32
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_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
[AgdaAny]
_ -> T_Dec_32
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_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
(:) AgdaAny
v5 [AgdaAny]
v6
-> let v7 :: t
v7 = (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v3 AgdaAny
v5 in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(let v8 :: t
v8 = ((AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32
du_decPointwise_36 ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
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_32
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v9 T_Reflects_14
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v10 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v11
-> case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v12 T_Reflects_14
v13
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v12
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v13 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v14
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v12)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v13)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v12)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_14
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v10)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
[AgdaAny]
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
[AgdaAny]
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'46'extendedlambda0_92 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
AgdaAny ->
[AgdaAny] ->
AgdaAny ->
[AgdaAny] ->
AgdaAny ->
(MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda0_92 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> (T_Pointwise_48 -> T_'8869'_4)
-> T_Pointwise_48
-> T_'8869'_4
d_'46'extendedlambda0_92 = ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> (T_Pointwise_48 -> T_'8869'_4)
-> T_Pointwise_48
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda1_108 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny -> ()) ->
(AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
AgdaAny ->
[AgdaAny] ->
AgdaAny ->
[AgdaAny] ->
(AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda1_108 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_'8869'_4)
-> T_Dec_32
-> T_Pointwise_48
-> T_'8869'_4
d_'46'extendedlambda1_108 = ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_'8869'_4)
-> T_Dec_32
-> T_Pointwise_48
-> T_'8869'_4
forall a. a
erased
d_decEq'45''8866'_116 ::
() ->
T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_decEq'45''8866'_116 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
d_decEq'45''8866'_116 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
= T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_decEq'45''8866'_116 ::
T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_decEq'45''8866'_116 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 T_DecEq_6
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 AgdaAny
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 AgdaAny
v4
-> let v5 :: t
v5 = (T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> T_DecEq_6 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 T_DecEq_6
v0 AgdaAny
v3 AgdaAny
v4 in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v6 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> let v5 :: t
v5
= (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 ((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Maybe_122 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0))
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v6 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v5 T__'8866'_14
v6
-> let v7 :: t
v7
= (T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 ((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T_DecEq_6
du_DecEq'45''8866'_138 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)) T__'8866'_14
v3 T__'8866'_14
v5)
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 ((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T_DecEq_6
du_DecEq'45''8866'_138 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)) T__'8866'_14
v4 T__'8866'_14
v6) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v8 T_Reflects_14
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v9 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v10
-> (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
v10)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
AgdaAny
forall a. a
erased))
T_Reflects_14
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v9)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> let v5 :: t
v5
= (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v6 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> let v5 :: t
v5
= (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v6 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
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 AgdaAny
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v4
-> let v5 :: T_Dec_32
v5 = T_TmCon_198 -> T_TmCon_198 -> T_Dec_32
d_decEq'45'TmCon_18 (T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v3) (T_TmCon_198 -> T_TmCon_198
forall a b. a -> b
coe T_TmCon_198
v4) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v5 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v6 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v5 T__'8866'_14
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v5 [T__'8866'_14]
v6
-> let v7 :: t
v7
= (T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
((Integer -> Integer -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8799'__1528 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5))
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> [T__'8866'_14] -> [T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 ((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List'45''8866'_144 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)) [T__'8866'_14]
v4
[T__'8866'_14]
v6) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v8 T_Reflects_14
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v9 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v10
-> (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
v10)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
AgdaAny
forall a. a
erased))
T_Reflects_14
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v9)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v5 T__'8866'_14
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v5 [T__'8866'_14]
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v5 [T__'8866'_14]
v6
-> let v7 :: t
v7
= (T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v5))
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> [T__'8866'_14] -> [T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 ((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List'45''8866'_144 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)) [T__'8866'_14]
v4
[T__'8866'_14]
v6) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v8 T_Reflects_14
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v9 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v10
-> (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
v10)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
AgdaAny
forall a. a
erased))
T_Reflects_14
_ -> 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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v9)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> let v5 :: T_Dec_32
v5
= T_Builtin_2 -> T_Builtin_2 -> T_Dec_32
MAlonzo.Code.Builtin.d_decBuiltin_398 (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe T_Builtin_2
v3) (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe T_Builtin_2
v4) in
AgdaAny -> T_Dec_32
forall a b. a -> b
coe
(case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v5 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v6 T_Reflects_14
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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v7)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v6)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_32
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 AgdaAny
v3
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v3
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v3 T__'8866'_14
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v3
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v3
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v3
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v3 [T__'8866'_14]
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v3 [T__'8866'_14]
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v3
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
forall a. a
erased)
T__'8866'_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
d_DecEq'45'Maybe_122 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'Maybe_122 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'Maybe_122 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Maybe_122 T_DecEq_6
v1
du_DecEq'45'Maybe_122 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Maybe_122 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'Maybe_122 T_DecEq_6
v0
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11
(((AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_32
MAlonzo.Code.Data.Maybe.Properties.du_'8801''45'dec_24
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_32
d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)))
d_EmptyEq_128 :: T_DecEq_6
d_EmptyEq_128 :: T_DecEq_6
d_EmptyEq_128 = ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11 AgdaAny
forall a. a
erased
d_DecAtomicTyCon_130 :: T_DecEq_6
d_DecAtomicTyCon_130 :: T_DecEq_6
d_DecAtomicTyCon_130
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11
((T_AtomicTyCon_6 -> T_AtomicTyCon_6 -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe T_AtomicTyCon_6 -> T_AtomicTyCon_6 -> T_Dec_32
MAlonzo.Code.Builtin.Constant.AtomicType.d_decAtomicTyCon_26)
d_DecEq'45'TmCon_132 :: T_DecEq_6
d_DecEq'45'TmCon_132 :: T_DecEq_6
d_DecEq'45'TmCon_132
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11 ((T_TmCon_198 -> T_TmCon_198 -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe T_TmCon_198 -> T_TmCon_198 -> T_Dec_32
d_decEq'45'TmCon_18)
d_DecEq'45''8866'_138 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45''8866'_138 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45''8866'_138 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T_DecEq_6
du_DecEq'45''8866'_138 T_DecEq_6
v1
du_DecEq'45''8866'_138 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45''8866'_138 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45''8866'_138 T_DecEq_6
v0
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11 ((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0))
d_DecEq'45'List'45''8866'_144 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'List'45''8866'_144 :: () -> T_DecEq_6 -> T_DecEq_6
d_DecEq'45'List'45''8866'_144 ~()
v0 T_DecEq_6
v1
= T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List'45''8866'_144 T_DecEq_6
v1
du_DecEq'45'List'45''8866'_144 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List'45''8866'_144 :: T_DecEq_6 -> T_DecEq_6
du_DecEq'45'List'45''8866'_144 T_DecEq_6
v0
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11
(((AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32
MAlonzo.Code.Data.List.Properties.du_'8801''45'dec_54
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_decEq'45''8866'_116 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0)))
d_DecEq'45'Builtin_146 :: T_DecEq_6
d_DecEq'45'Builtin_146 :: T_DecEq_6
d_DecEq'45'Builtin_146
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11
((T_Builtin_2 -> T_Builtin_2 -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe T_Builtin_2 -> T_Builtin_2 -> T_Dec_32
MAlonzo.Code.Builtin.d_decBuiltin_398)
d_DecEq'45'ℕ_148 :: T_DecEq_6
d_DecEq'45'ℕ_148 :: T_DecEq_6
d_DecEq'45'ℕ_148
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11
((Integer -> Integer -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Nat.Properties.d__'8799'__1528)
d_DecEq'45'ℤ_150 :: T_DecEq_6
d_DecEq'45'ℤ_150 :: T_DecEq_6
d_DecEq'45'ℤ_150
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11
((Integer -> Integer -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> T_Dec_32
MAlonzo.Code.Data.Integer.Properties.d__'8799'__1540)
d_DecEq'45'TyTag_152 :: T_DecEq_6
d_DecEq'45'TyTag_152 :: T_DecEq_6
d_DecEq'45'TyTag_152
= ((AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6)
-> AgdaAny -> T_DecEq_6
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_32) -> T_DecEq_6
C_DecEq'46'constructor_11 ((T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_32) -> AgdaAny
forall a b. a -> b
coe T__'8866''9839'_4 -> T__'8866''9839'_4 -> T_Dec_32
d_decEq'45'TyTag_20)
d_'46'extendedlambda2_172 ::
MAlonzo.Code.Builtin.Constant.AtomicType.T_AtomicTyCon_6 ->
MAlonzo.Code.Builtin.Constant.AtomicType.T_AtomicTyCon_6 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda2_172 :: T_AtomicTyCon_6
-> T_AtomicTyCon_6
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda2_172 = T_AtomicTyCon_6
-> T_AtomicTyCon_6
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda3_206 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda3_206 :: T__'8866''9839'_4
-> T__'8866''9839'_4
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda3_206 = T__'8866''9839'_4
-> T__'8866''9839'_4
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda4_256 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda4_256 :: T__'8866''9839'_4
-> T__'8866''9839'_4
-> T__'8866''9839'_4
-> T__'8866''9839'_4
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda4_256 = T__'8866''9839'_4
-> T__'8866''9839'_4
-> T__'8866''9839'_4
-> T__'8866''9839'_4
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_HsEq_260 :: p -> ()
d_HsEq_260 p
a0 = ()
newtype T_HsEq_260
= C_HsEq'46'constructor_31555 (AgdaAny -> AgdaAny -> Bool)
d_hsEq_266 :: T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_266 :: T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_266 T_HsEq_260
v0
= case T_HsEq_260 -> T_HsEq_260
forall a b. a -> b
coe T_HsEq_260
v0 of
C_HsEq'46'constructor_31555 AgdaAny -> AgdaAny -> Bool
v1 -> (AgdaAny -> AgdaAny -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Bool
v1
T_HsEq_260
_ -> AgdaAny -> AgdaAny -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
d_hsEq_270 :: T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_270 :: T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_270 T_HsEq_260
v0 = (T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool)
-> AgdaAny -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_266 (T_HsEq_260 -> AgdaAny
forall a b. a -> b
coe T_HsEq_260
v0)
d_magicNeg_278 :: a
d_magicNeg_278
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: VerifiedCompilation.Equality.magicNeg"
d_magicBoolDec_286 ::
() ->
AgdaAny ->
AgdaAny -> Bool -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_magicBoolDec_286 :: () -> AgdaAny -> AgdaAny -> Bool -> T_Dec_32
d_magicBoolDec_286 ~()
v0 ~AgdaAny
v1 ~AgdaAny
v2 Bool
v3 = Bool -> T_Dec_32
du_magicBoolDec_286 Bool
v3
du_magicBoolDec_286 ::
Bool -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_magicBoolDec_286 :: Bool -> T_Dec_32
du_magicBoolDec_286 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
forall a. a
erased)
else (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
d_builtinEq_292 ::
() ->
T_HsEq_260 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_builtinEq_292 :: () -> T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32
d_builtinEq_292 ~()
v0 T_HsEq_260
v1 AgdaAny
v2 AgdaAny
v3 = T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32
du_builtinEq_292 T_HsEq_260
v1 AgdaAny
v2 AgdaAny
v3
du_builtinEq_292 ::
T_HsEq_260 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_builtinEq_292 :: T_HsEq_260 -> AgdaAny -> AgdaAny -> T_Dec_32
du_builtinEq_292 T_HsEq_260
v0 AgdaAny
v1 AgdaAny
v2
= (Bool -> T_Dec_32) -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe Bool -> T_Dec_32
du_magicBoolDec_286 ((T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool)
-> T_HsEq_260 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_HsEq_260 -> AgdaAny -> AgdaAny -> Bool
d_hsEq_266 T_HsEq_260
v0 AgdaAny
v1 AgdaAny
v2)
d_HsEqBytestring_298 :: T_HsEq_260
d_HsEqBytestring_298 :: T_HsEq_260
d_HsEqBytestring_298
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260)
-> AgdaAny -> T_HsEq_260
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_ByteString_356 -> T_ByteString_356 -> Bool) -> AgdaAny
forall a b. a -> b
coe T_ByteString_356 -> T_ByteString_356 -> Bool
MAlonzo.Code.Utils.d_eqByteString_358)
d_HsEqBlsG1_300 :: T_HsEq_260
d_HsEqBlsG1_300 :: T_HsEq_260
d_HsEqBlsG1_300
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260)
-> AgdaAny -> T_HsEq_260
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_Bls12'45'381'45'G1'45'Element_464
-> T_Bls12'45'381'45'G1'45'Element_464 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'G1'45'Element_464
-> T_Bls12'45'381'45'G1'45'Element_464 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'G1'45'Element_466)
d_HsEqBlsG2_302 :: T_HsEq_260
d_HsEqBlsG2_302 :: T_HsEq_260
d_HsEqBlsG2_302
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260)
-> AgdaAny -> T_HsEq_260
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_Bls12'45'381'45'G2'45'Element_468
-> T_Bls12'45'381'45'G2'45'Element_468 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'G2'45'Element_468
-> T_Bls12'45'381'45'G2'45'Element_468 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'G2'45'Element_470)
d_HsEqBlsMlResult_304 :: T_HsEq_260
d_HsEqBlsMlResult_304 :: T_HsEq_260
d_HsEqBlsMlResult_304
= ((AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260)
-> AgdaAny -> T_HsEq_260
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> Bool) -> T_HsEq_260
C_HsEq'46'constructor_31555
((T_Bls12'45'381'45'MlResult_472
-> T_Bls12'45'381'45'MlResult_472 -> Bool)
-> AgdaAny
forall a b. a -> b
coe T_Bls12'45'381'45'MlResult_472
-> T_Bls12'45'381'45'MlResult_472 -> Bool
MAlonzo.Code.Utils.d_eqBls12'45'381'45'MlResult_474)
d_'46'extendedlambda5_350 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Utils.T_List_382 AgdaAny ->
MAlonzo.Code.Utils.T_List_382 AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda5_350 :: T__'8866''9839'_4
-> AgdaAny
-> AgdaAny
-> (T__'8801'__12 -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda5_350 = T__'8866''9839'_4
-> AgdaAny
-> AgdaAny
-> (T__'8801'__12 -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda6_388 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Utils.T_List_382 AgdaAny ->
MAlonzo.Code.Utils.T_List_382 AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda6_388 :: T__'8866''9839'_4
-> [AgdaAny]
-> [AgdaAny]
-> (T__'8801'__12 -> T_'8869'_4)
-> AgdaAny
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda6_388 = T__'8866''9839'_4
-> [AgdaAny]
-> [AgdaAny]
-> (T__'8801'__12 -> T_'8869'_4)
-> AgdaAny
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda7_432 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda7_432 :: T__'8866''9839'_4
-> T__'8866''9839'_4
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda7_432 = T__'8866''9839'_4
-> T__'8866''9839'_4
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda8_456 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda8_456 :: T__'8866''9839'_4
-> T__'8866''9839'_4
-> (T__'8801'__12 -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda8_456 = T__'8866''9839'_4
-> T__'8866''9839'_4
-> (T__'8801'__12 -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda9_488 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda9_488 :: T__'8866''9839'_4
-> AgdaAny
-> AgdaAny
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda9_488 = T__'8866''9839'_4
-> AgdaAny
-> AgdaAny
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda10_508 ::
() ->
T_DecEq_6 ->
AgdaAny ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda10_508 :: ()
-> T_DecEq_6
-> AgdaAny
-> AgdaAny
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda10_508 = ()
-> T_DecEq_6
-> AgdaAny
-> AgdaAny
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda11_574 ::
() ->
T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda11_574 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda11_574 = ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda12_654 ::
() ->
T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda12_654 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda12_654 = ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda13_732 ::
() ->
T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda13_732 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda13_732 = ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda14_796 ::
() ->
T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda14_796 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda14_796 = ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T__'8801'__12 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda15_860 ::
MAlonzo.Code.RawU.T_TmCon_198 ->
MAlonzo.Code.RawU.T_TmCon_198 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
() ->
T_DecEq_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda15_860 :: T_TmCon_198
-> T_TmCon_198
-> (T__'8801'__12 -> T_'8869'_4)
-> ()
-> T_DecEq_6
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda15_860 = T_TmCon_198
-> T_TmCon_198
-> (T__'8801'__12 -> T_'8869'_4)
-> ()
-> T_DecEq_6
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda16_948 ::
() ->
T_DecEq_6 ->
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda16_948 :: ()
-> T_DecEq_6
-> Integer
-> [T__'8866'_14]
-> Integer
-> [T__'8866'_14]
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda16_948 = ()
-> T_DecEq_6
-> Integer
-> [T__'8866'_14]
-> Integer
-> [T__'8866'_14]
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda17_1044 ::
() ->
T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda17_1044 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> [T__'8866'_14]
-> T__'8866'_14
-> [T__'8866'_14]
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda17_1044 = ()
-> T_DecEq_6
-> T__'8866'_14
-> [T__'8866'_14]
-> T__'8866'_14
-> [T__'8866'_14]
-> (T_Σ_14 -> T_'8869'_4)
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased
d_'46'extendedlambda18_1112 ::
MAlonzo.Code.Builtin.T_Builtin_2 ->
MAlonzo.Code.Builtin.T_Builtin_2 ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4) ->
() ->
T_DecEq_6 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Data.Empty.T_'8869'_4
d_'46'extendedlambda18_1112 :: T_Builtin_2
-> T_Builtin_2
-> (T__'8801'__12 -> T_'8869'_4)
-> ()
-> T_DecEq_6
-> T__'8801'__12
-> T_'8869'_4
d_'46'extendedlambda18_1112 = T_Builtin_2
-> T_Builtin_2
-> (T__'8801'__12 -> T_'8869'_4)
-> ()
-> T_DecEq_6
-> T__'8801'__12
-> T_'8869'_4
forall a. a
erased