{-# 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.UFloatDelay 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.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.Maybe.Properties
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.VerifiedCompilation.Equality
import qualified MAlonzo.Code.VerifiedCompilation.Purity
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews
d_AllForced_18 :: p -> p -> p -> p -> ()
d_AllForced_18 p
a0 p
a1 p
a2 p
a3 = ()
data T_AllForced_18
= C_var_28 | C_forced_32 | C_force_36 T_AllForced_18 |
C_delay_40 T_AllForced_18 | C_ƛ_46 T_AllForced_18 |
C_app_50 T_AllForced_18 T_AllForced_18 | C_error_54 |
C_builtin_60 | C_con_66 |
C_case_74 T_AllForced_18
MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 |
C_constr_82 MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_isAllForced'63'_90 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isAllForced'63'_90 :: () -> T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
d_isAllForced'63'_90 ~()
v0 T_DecEq_6
v1 AgdaAny
v2 T__'8866'_14
v3 = T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 T_DecEq_6
v1 AgdaAny
v2 T__'8866'_14
v3
du_isAllForced'63'_90 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isAllForced'63'_90 :: T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 T_DecEq_6
v0 AgdaAny
v1 T__'8866'_14
v2
= let v3 :: t
v3
= (()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> t
forall a b. a -> b
coe
() -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isForce'63'_284
AgdaAny
forall a. a
erased
(\ AgdaAny
v3 AgdaAny
v4 ->
T_Dec_20 -> AgdaAny
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v6
-> case AgdaAny -> T_isForce_268
forall a b. a -> b
coe AgdaAny
v6 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 AgdaAny
v8
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v9
-> (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
v8)
(let v10 :: t
v10
= (T__'8866'_14 -> T_Dec_20) -> AgdaAny -> t
forall a b. a -> b
coe
T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isVar'63'_24
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v9) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v12 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v13
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
(case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v9 of
MAlonzo.Code.Untyped.C_'96'_18 AgdaAny
v14
-> let v15 :: t
v15
= (T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecEq_6 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.d__'8799'__12
T_DecEq_6
v0 AgdaAny
v14
AgdaAny
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v15 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v16 T_Reflects_16
v17
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v16
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
v17)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe
Bool
v16)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_AllForced_18 -> AgdaAny
forall a b. a -> b
coe
T_AllForced_18
C_forced_32)))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
v17)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe
Bool
v11)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_AllForced_18 -> T_AllForced_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_AllForced_18 -> T_AllForced_18
C_force_36
(T_AllForced_18 -> AgdaAny
forall a b. a -> b
coe
T_AllForced_18
C_var_28))))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v12)
(let v13 :: t
v13
= (T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90
(T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v9) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v13 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v14 T_Reflects_16
v15
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v14
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v15 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v16
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v14)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_AllForced_18 -> T_AllForced_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_AllForced_18 -> T_AllForced_18
C_force_36
AgdaAny
v16))
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v15)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v14)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isForce_268
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v6
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
(let v7 :: t
v7
= (T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> T_DecEq_6 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.d__'8799'__12 T_DecEq_6
v0
AgdaAny
v6 AgdaAny
v1 in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v8 T_Reflects_16
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v9)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v9)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_AllForced_18 -> AgdaAny
forall a b. a -> b
coe T_AllForced_18
C_var_28)))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v6
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
(let v7 :: t
v7
= (T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90
((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0))
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v8 T_Reflects_16
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v9 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v10
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_AllForced_18 -> T_AllForced_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AllForced_18 -> T_AllForced_18
C_ƛ_46 AgdaAny
v10))
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v9)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v6 T__'8866'_14
v7
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
(let v8 :: t
v8
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v6))
((T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v7)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v10 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v11
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v11 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v12 AgdaAny
v13
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_AllForced_18 -> T_AllForced_18 -> T_AllForced_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AllForced_18 -> T_AllForced_18 -> T_AllForced_18
C_app_50 AgdaAny
v12 AgdaAny
v13))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v6
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v6
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
(let v7 :: t
v7 = (T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v6) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v8 T_Reflects_16
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v9 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v10
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_AllForced_18 -> T_AllForced_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AllForced_18 -> T_AllForced_18
C_delay_40 AgdaAny
v10))
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v9)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v6
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_AllForced_18 -> AgdaAny
forall a b. a -> b
coe T_AllForced_18
C_con_66)))
MAlonzo.Code.Untyped.C_constr_34 Integer
v6 [T__'8866'_14]
v7
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
(let v8 :: t
v8
= ((AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
(AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Unary.All.du_all'63'_506
((T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v7) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v10 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v11
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_All_44 -> T_AllForced_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_All_44 -> T_AllForced_18
C_constr_82 AgdaAny
v11))
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v6 [T__'8866'_14]
v7
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
(let v8 :: t
v8
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v6))
(((AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Dec_20) -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Unary.All.du_all'63'_506
((T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> AgdaAny -> T__'8866'_14 -> T_Dec_20
du_isAllForced'63'_90 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v7)) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v10 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v11
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v11 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v12 AgdaAny
v13
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_AllForced_18 -> T_All_44 -> T_AllForced_18)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_AllForced_18 -> T_All_44 -> T_AllForced_18
C_case_74 AgdaAny
v12 AgdaAny
v13))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v10)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v6
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_AllForced_18 -> AgdaAny
forall a b. a -> b
coe T_AllForced_18
C_builtin_60)))
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_AllForced_18 -> AgdaAny
forall a b. a -> b
coe T_AllForced_18
C_error_54)))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'46'extendedlambda0_142 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
(T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isVar_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_142 :: ()
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_AllForced_18 -> T_Irrelevant_20)
-> (T_isVar_14 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda0_142 = ()
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_AllForced_18 -> T_Irrelevant_20)
-> (T_isVar_14 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda1_186 ::
() ->
AgdaAny ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_186 :: ()
-> AgdaAny
-> T_DecEq_6
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda1_186 = ()
-> AgdaAny
-> T_DecEq_6
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda2_230 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
(T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda2_230 :: ()
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_AllForced_18 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda2_230 = ()
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_AllForced_18 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda3_268 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda3_268 :: ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_Σ_14 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda3_268 = ()
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_Σ_14 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda4_280 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda4_280 :: ()
-> T__'8866'_14
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_DecEq_6
-> AgdaAny
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda4_280 = ()
-> T__'8866'_14
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_DecEq_6
-> AgdaAny
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda5_310 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
(T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda5_310 :: ()
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_AllForced_18 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda5_310 = ()
-> T__'8866'_14
-> T_DecEq_6
-> AgdaAny
-> (T_AllForced_18 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda6_352 ::
() ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
(MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
Integer ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda6_352 :: ()
-> [T__'8866'_14]
-> T_DecEq_6
-> AgdaAny
-> (T_All_44 -> T_Irrelevant_20)
-> Integer
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda6_352 = ()
-> [T__'8866'_14]
-> T_DecEq_6
-> AgdaAny
-> (T_All_44 -> T_Irrelevant_20)
-> Integer
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda7_390 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
AgdaAny ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_268 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_AllForced_18 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda7_390 :: ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T_DecEq_6
-> AgdaAny
-> (T_Σ_14 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
d_'46'extendedlambda7_390 = ()
-> T__'8866'_14
-> [T__'8866'_14]
-> T_DecEq_6
-> AgdaAny
-> (T_Σ_14 -> T_Irrelevant_20)
-> (T_isForce_268 -> T_Irrelevant_20)
-> T_AllForced_18
-> T_Irrelevant_20
forall a. a
erased
d_subs'45'delay_412 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Maybe AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14
d_subs'45'delay_412 :: () -> T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
d_subs'45'delay_412 ~()
v0 T_DecEq_6
v1 Maybe AgdaAny
v2 T__'8866'_14
v3 = T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 T_DecEq_6
v1 Maybe AgdaAny
v2 T__'8866'_14
v3
du_subs'45'delay_412 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
Maybe AgdaAny ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14
du_subs'45'delay_412 :: T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 T_DecEq_6
v0 Maybe AgdaAny
v1 T__'8866'_14
v2
= 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
-> let v4 :: t
v4
= ((AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> T_Dec_20)
-> Maybe AgdaAny -> Maybe AgdaAny -> T_Dec_20
MAlonzo.Code.Data.Maybe.Properties.du_'8801''45'dec_24
((T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.d__'8799'__12 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0))
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) in
AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v4 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6)
((T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26
((AgdaAny -> T__'8866'_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8866'_14
MAlonzo.Code.Untyped.C_'96'_18 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1)))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v6) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2)
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v3
-> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_ƛ_20
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412
((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0))
((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1)) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v3 T__'8866'_14
v4
-> (T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v4))
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v3
-> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v3
-> (T__'8866'_14 -> T__'8866'_14) -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
MAlonzo.Code.Untyped.C_con_28 T_TmCon_198
v3 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2
MAlonzo.Code.Untyped.C_constr_34 Integer
v3 [T__'8866'_14]
v4
-> (Integer -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
Integer -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_constr_34 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)
(((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1)) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v4))
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v3 [T__'8866'_14]
v4
-> (T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1) (T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v3))
(((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412 (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1)) ([T__'8866'_14] -> AgdaAny
forall a b. a -> b
coe [T__'8866'_14]
v4))
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v3 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 -> T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2
T__'8866'_14
_ -> T__'8866'_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_FlD_474 :: p -> p -> p -> p -> ()
d_FlD_474 p
a0 p
a1 p
a2 p
a3 = ()
data T_FlD_474
= C_floatdelay_488 MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_16
MAlonzo.Code.VerifiedCompilation.Purity.T_UPure_6
d_FloatDelay_498 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_FloatDelay_498 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_FloatDelay_498 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
d_isFloatDelay'63'_504 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isFloatDelay'63'_504 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_isFloatDelay'63'_504 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isFloatDelay'63'_504 T_DecEq_6
v1
du_isFloatDelay'63'_504 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isFloatDelay'63'_504 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isFloatDelay'63'_504 T_DecEq_6
v0
= (()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_20
forall a b. a -> b
coe
()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_100
AgdaAny
forall a. a
erased (T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe T_DecEq_6
v0) (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isFlD'63'_510 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4)
d_isFlD'63'_510 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isFlD'63'_510 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_isFlD'63'_510 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isFlD'63'_510 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isFlD'63'_510 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isFlD'63'_510 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isFlD'63'_510 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
= let v3 :: t
v3
= (()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
AgdaAny
forall a. a
erased
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 ->
((() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_70
(\ AgdaAny
v4 AgdaAny
v5 ->
T_Dec_20 -> AgdaAny
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
() -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isDelay'63'_370
AgdaAny
forall a. a
erased
(\ AgdaAny
v4 AgdaAny
v5 ->
T_Dec_20 -> AgdaAny
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v1) in
AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v6
-> case AgdaAny -> T_isApp_142
forall a b. a -> b
coe AgdaAny
v6 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 AgdaAny
v9 AgdaAny
v10
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v11 T__'8866'_14
v12
-> case AgdaAny -> T_isLambda_54
forall a b. a -> b
coe AgdaAny
v9 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_62 AgdaAny
v14
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v11 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v15
-> (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
v14)
(case AgdaAny -> T_isDelay_354
forall a b. a -> b
coe AgdaAny
v10 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_362 AgdaAny
v17
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v12 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v18
-> (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
v17)
(let v19 :: t
v19
= (()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> t
forall a b. a -> b
coe
()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
AgdaAny
forall a. a
erased
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v19 ->
((() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_70
(\ AgdaAny
v20
AgdaAny
v21 ->
T_Dec_20 -> AgdaAny
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
(\ AgdaAny
v19 AgdaAny
v20 ->
T_Dec_20 -> AgdaAny
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe T__'8866'_14
v2) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v20 T_Reflects_16
v21
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v20
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v21 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v22
-> case AgdaAny -> T_isApp_142
forall a b. a -> b
coe
AgdaAny
v22 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 AgdaAny
v25 AgdaAny
v26
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v27 T__'8866'_14
v28
-> case AgdaAny -> T_isLambda_54
forall a b. a -> b
coe
AgdaAny
v25 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_62 AgdaAny
v30
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v27 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v31
-> (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
v30)
((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
v26)
(let v32 :: t
v32
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isFloatDelay'63'_504
((T_DecEq_6 -> T_DecEq_6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6
v0))
((T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> Maybe AgdaAny -> T__'8866'_14 -> T__'8866'_14
du_subs'45'delay_412
(T_DecEq_6 -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6
v0)
(Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
(T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T__'8866'_14
v15))
T__'8866'_14
v31)
((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> AgdaAny
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isFloatDelay'63'_504
T_DecEq_6
v0
T__'8866'_14
v18
T__'8866'_14
v28)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe
Bool
v20)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_UPure_6 -> AgdaAny
forall a b. a -> b
coe
T_UPure_6
MAlonzo.Code.VerifiedCompilation.Purity.C_FIXME_12)))) in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Dec_20
forall a b. a -> b
coe
AgdaAny
forall a. a
v32 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v33 T_Reflects_16
v34
-> if Bool -> Bool
forall a b. a -> b
coe
Bool
v33
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v34 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v35
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny
v35 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v36 AgdaAny
v37
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe
AgdaAny
v37 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v38 AgdaAny
v39
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe
Bool
v33)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_Translation_16 -> T_Translation_16 -> T_UPure_6 -> T_FlD_474)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Translation_16 -> T_Translation_16 -> T_UPure_6 -> T_FlD_474
C_floatdelay_488
AgdaAny
v36
AgdaAny
v38
AgdaAny
v39))
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
v34)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe
Bool
v33)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isLambda_54
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
v21)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe
Bool
v20)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isDelay_354
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isLambda_54
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v5)
((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'46'extendedlambda8_526 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_FlD_474 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda8_526 :: ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_FlD_474
-> T_Irrelevant_20
d_'46'extendedlambda8_526 = ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T_DecEq_6
-> T__'8866'_14
-> T_FlD_474
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda9_556 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isApp_142 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
T_FlD_474 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda9_556 :: ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> T_FlD_474
-> T_Irrelevant_20
d_'46'extendedlambda9_556 = ()
-> T__'8866'_14
-> (T_isApp_142 -> T_Irrelevant_20)
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> T_FlD_474
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda10_594 ::
() ->
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.VerifiedCompilation.Equality.T_DecEq_6 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_FlD_474 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda10_594 :: ()
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_FlD_474
-> T_Irrelevant_20
d_'46'extendedlambda10_594 = ()
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T__'8866'_14
-> T_DecEq_6
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_FlD_474
-> T_Irrelevant_20
forall a. a
erased