{-# 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.UCaseOfCase 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.Sigma
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.Nat.Properties
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.UntypedTranslation
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews
d_CoC_4 :: p -> p -> p -> p -> ()
d_CoC_4 p
a0 p
a1 p
a2 p
a3 = ()
data T_CoC_4
= C_isCoC_28 MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_CaseOfCase_38 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_CaseOfCase_38 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_CaseOfCase_38 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
d_CoCCase_42 :: p -> p -> ()
d_CoCCase_42 p
a0 p
a1 = ()
data T_CoCCase_42 = C_isCoCCase_58
d_isCoCCase'63'_62 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isCoCCase'63'_62 :: () -> T__'8866'_14 -> T_Dec_20
d_isCoCCase'63'_62 ~()
v0 T__'8866'_14
v1 = T__'8866'_14 -> T_Dec_20
du_isCoCCase'63'_62 T__'8866'_14
v1
du_isCoCCase'63'_62 ::
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isCoCCase'63'_62 :: T__'8866'_14 -> T_Dec_20
du_isCoCCase'63'_62 T__'8866'_14
v0
= let v1 :: t
v1
= (()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any -> 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_isCase'63'_598
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> Any -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> Any -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v4 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
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
Any
forall a. a
erased
(\ Any
v5 Any
v6 ->
(T__'8866'_14 -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isBuiltin'63'_708
Any
v6)))
(\ Any
v4 Any
v5 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
Any
forall a. a
erased
(\ Any
v4 Any
v5 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
(()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
Any
forall a. a
erased
(\ Any
v3 Any
v4 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))
(\ Any
v1 Any
v2 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v0) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v1 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v2 T_Reflects_16
v3
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v3 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v4
-> case Any -> T_isCase_574
forall a b. a -> b
coe Any
v4 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v7 Any
v8
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v9 [T__'8866'_14]
v10
-> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v13 Any
v14
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v9 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v15 T__'8866'_14
v16
-> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v13 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v19 Any
v20
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v15 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v21 T__'8866'_14
v22
-> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v19 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v25 Any
v26
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v21 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v27 T__'8866'_14
v28
-> case Any -> T_isForce_268
forall a b. a -> b
coe Any
v25 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 Any
v30
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v27 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v31
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v30)
(case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v31 of
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v32
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v26)
(case Any -> T_isConstr_478
forall a b. a -> b
coe
Any
v20 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v35
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v35)
(case Any -> T_isConstr_478
forall a b. a -> b
coe
Any
v14 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v38
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v38)
((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v8)
(let v39 :: T_Dec_20
v39
= T_Builtin_2 -> T_Builtin_2 -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_398
(T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe
T_Builtin_2
v32)
(T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe
T_Builtin_2
MAlonzo.Code.Builtin.C_ifThenElse_60) in
Any -> Any
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe
T_Dec_20
v39 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v40 T_Reflects_16
v41
-> if Bool -> Bool
forall a b. a -> b
coe
Bool
v40
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
v41)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe
Bool
v40)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_CoCCase_42 -> Any
forall a b. a -> b
coe
T_CoCCase_42
C_isCoCCase_58)))
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
v41)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe
Bool
v40)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isForce_268
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v3)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v2)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_CoCForce_146 :: p -> p -> ()
d_CoCForce_146 p
a0 p
a1 = ()
data T_CoCForce_146 = C_isCoCForce_162
d_isCoCForce'63'_168 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isCoCForce'63'_168 :: () -> T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
d_isCoCForce'63'_168 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 = T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
du_isCoCForce'63'_168 T_DecEq_6
v1 T__'8866'_14
v2
du_isCoCForce'63'_168 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isCoCForce'63'_168 :: T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
du_isCoCForce'63'_168 T_DecEq_6
v0 T__'8866'_14
v1
= let v2 :: t
v2
= (()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any -> 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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v2 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> Any -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> Any -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v4 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v5 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
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
Any
forall a. a
erased
(\ Any
v6 Any
v7 ->
(T__'8866'_14 -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isBuiltin'63'_708
Any
v7)))
(\ Any
v5 Any
v6 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v4 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v5 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
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_isCase'63'_598
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v6 ->
(()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
Any
forall a. a
erased
(\ Any
v7 Any
v8 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))
(\ Any
v6 Any
v7 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))))
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v3 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any
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
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v4 ->
(()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
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_isCase'63'_598
Any
forall a. a
erased
((Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v5 ->
(()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
Any
forall a. a
erased
(\ Any
v6 Any
v7 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))
(\ Any
v5 Any
v6 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
forall a. a
v2 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v4 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v5
-> case Any -> T_isForce_268
forall a b. a -> b
coe Any
v5 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 Any
v7
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v8
-> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v11 Any
v12
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v8 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v13 T__'8866'_14
v14
-> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v11 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v17 Any
v18
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v13 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v19 T__'8866'_14
v20
-> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v17 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v23 Any
v24
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v19 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v25 T__'8866'_14
v26
-> case Any -> T_isForce_268
forall a b. a -> b
coe Any
v23 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 Any
v28
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v25 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v29
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v28)
(case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v29 of
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v30
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v24)
(case Any -> T_isDelay_354
forall a b. a -> b
coe
Any
v18 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_362 Any
v32
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v20 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v33
-> case Any -> T_isCase_574
forall a b. a -> b
coe
Any
v32 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v36 Any
v37
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v33 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v38 [T__'8866'_14]
v39
-> case Any -> T_isConstr_478
forall a b. a -> b
coe
Any
v36 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v42
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v42)
((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v37)
(case Any -> T_isDelay_354
forall a b. a -> b
coe
Any
v12 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_362 Any
v44
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v14 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v45
-> case Any -> T_isCase_574
forall a b. a -> b
coe
Any
v44 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v48 Any
v49
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v45 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v50 [T__'8866'_14]
v51
-> case Any -> T_isConstr_478
forall a b. a -> b
coe
Any
v48 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v54
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v54)
((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v49)
(let v55 :: t
v55
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> 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_Builtin_2 -> T_Builtin_2 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Builtin_2 -> T_Builtin_2 -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_398
(T_Builtin_2 -> Any
forall a b. a -> b
coe
T_Builtin_2
v30)
(T_Builtin_2 -> Any
forall a b. a -> b
coe
T_Builtin_2
MAlonzo.Code.Builtin.C_ifThenElse_60))
((T_DecEq_6 -> Any -> Any -> T_Dec_20)
-> Any -> [T__'8866'_14] -> [T__'8866'_14] -> Any
forall a b. a -> b
coe
T_DecEq_6 -> Any -> Any -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.d__'8799'__12
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'List'45''8866'_144
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0))
[T__'8866'_14]
v39
[T__'8866'_14]
v51) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe
Any
forall a. a
v55 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v56 T_Reflects_16
v57
-> if Bool -> Bool
forall a b. a -> b
coe
Bool
v56
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v57 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v58
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(Any -> Any
forall a b. a -> b
coe
Any
v58)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe
Bool
v56)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_CoCForce_146 -> Any
forall a b. a -> b
coe
T_CoCForce_146
C_isCoCForce_162)))
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
v57)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe
Bool
v56)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isDelay_354
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isDelay_354
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isForce_268
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isForce_268
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v3)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_isCaseOfCase'63'_260 ::
() ->
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_isCaseOfCase'63'_260 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_isCaseOfCase'63'_260 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isCaseOfCase'63'_260 T_DecEq_6
v1
du_isCaseOfCase'63'_260 ::
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_isCaseOfCase'63'_260 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isCaseOfCase'63'_260 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)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any)
-> 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
Any
forall a. a
erased (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (\ Any
v1 Any
v2 Any
v3 Any
v4 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isCoC'63'_266 Any
v2 Any
v3 Any
v4)
d_isCoC'63'_266 ::
() ->
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_isCoC'63'_266 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
d_isCoC'63'_266 ~()
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_isCoC'63'_266 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isCoC'63'_266 ::
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_isCoC'63'_266 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isCoC'63'_266 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
= let v3 :: t
v3
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> 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__'8866'_14 -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T_Dec_20
du_isCoCCase'63'_62 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1))
((T_DecEq_6 -> T__'8866'_14 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
du_isCoCForce'63'_168 (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2)) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
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 Any
v6
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v7 Any
v8
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v7)
(case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v9 [T__'8866'_14]
v10
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v9 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v11 T__'8866'_14
v12
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v11 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v13 T__'8866'_14
v14
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v13 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v15 T__'8866'_14
v16
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v14 of
MAlonzo.Code.Untyped.C_constr_34 Integer
v17 [T__'8866'_14]
v18
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v12 of
MAlonzo.Code.Untyped.C_constr_34 Integer
v19 [T__'8866'_14]
v20
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
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
v21
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v21 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v22 T__'8866'_14
v23
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v22 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v24 T__'8866'_14
v25
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v24 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v26 T__'8866'_14
v27
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v25 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v28
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v28 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v29 [T__'8866'_14]
v30
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v29 of
MAlonzo.Code.Untyped.C_constr_34 Integer
v31 [T__'8866'_14]
v32
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v23 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v33
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v33 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v34 [T__'8866'_14]
v35
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14
v34 of
MAlonzo.Code.Untyped.C_constr_34 Integer
v36 [T__'8866'_14]
v37
-> let v38 :: t
v38
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> 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 -> Any -> Any -> T_Dec_20)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
T_DecEq_6 -> Any -> Any -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.d__'8799'__12
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45''8866'_138
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0))
T__'8866'_14
v16
T__'8866'_14
v27)
((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
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
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
(Integer -> Any
forall a b. a -> b
coe
Integer
v17)
(Integer -> Any
forall a b. a -> b
coe
Integer
v31))
((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
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
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
(Integer -> Any
forall a b. a -> b
coe
Integer
v19)
(Integer -> Any
forall a b. a -> b
coe
Integer
v36))
((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
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
(((Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.du_decPointwise_36
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isCaseOfCase'63'_260
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0))
([T__'8866'_14] -> Any
forall a b. a -> b
coe
[T__'8866'_14]
v18)
([T__'8866'_14] -> Any
forall a b. a -> b
coe
[T__'8866'_14]
v32))
((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
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
(((Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.du_decPointwise_36
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isCaseOfCase'63'_260
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0))
([T__'8866'_14] -> Any
forall a b. a -> b
coe
[T__'8866'_14]
v20)
([T__'8866'_14] -> Any
forall a b. a -> b
coe
[T__'8866'_14]
v37))
(((Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> T_Dec_20) -> [Any] -> [Any] -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.du_decPointwise_36
((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_20
du_isCaseOfCase'63'_260
(T_DecEq_6 -> Any
forall a b. a -> b
coe
T_DecEq_6
v0))
([T__'8866'_14] -> Any
forall a b. a -> b
coe
[T__'8866'_14]
v10)
([T__'8866'_14] -> Any
forall a b. a -> b
coe
[T__'8866'_14]
v30)))))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe
Any
forall a. a
v38 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v39 T_Reflects_16
v40
-> if Bool -> Bool
forall a b. a -> b
coe
Bool
v39
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
T_Reflects_16
v40 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v41
-> case Any -> T_Σ_14
forall a b. a -> b
coe
Any
v41 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v42 Any
v43
-> case Any -> T_Σ_14
forall a b. a -> b
coe
Any
v43 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v44 Any
v45
-> case Any -> T_Σ_14
forall a b. a -> b
coe
Any
v45 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v46 Any
v47
-> case Any -> T_Σ_14
forall a b. a -> b
coe
Any
v47 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v48 Any
v49
-> case Any -> T_Σ_14
forall a b. a -> b
coe
Any
v49 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v50 Any
v51
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe
Bool
v39)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 -> T_CoC_4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 -> T_CoC_4
C_isCoC_28
Any
v51
Any
v48
Any
v50))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
v40)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe
Bool
v39)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_'46'extendedlambda4_282 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_CoC_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda4_282 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_CoC_4
-> T_Irrelevant_20
d_'46'extendedlambda4_282 = ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_CoC_4
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda5_404 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
Integer ->
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
Integer ->
Integer ->
[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.Irrelevant.T_Irrelevant_20) ->
T_CoC_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda5_404 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_CoC_4
-> T_Irrelevant_20
d_'46'extendedlambda5_404 = ()
-> T_DecEq_6
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_CoC_4
-> T_Irrelevant_20
forall a. a
erased