{-# 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.Relation.Nullary.Decidable.Core 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.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Level
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d_Dec_20 :: p -> p -> ()
d_Dec_20 p
a0 p
a1 = ()
data T_Dec_20
= C__because__32 Bool
MAlonzo.Code.Relation.Nullary.Reflects.T_Reflects_16
d_does_28 :: T_Dec_20 -> Bool
d_does_28 :: T_Dec_20 -> Bool
d_does_28 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2 -> Bool -> Bool
forall a b. a -> b
coe Bool
v1
T_Dec_20
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
d_proof_30 ::
T_Dec_20 -> MAlonzo.Code.Relation.Nullary.Reflects.T_Reflects_16
d_proof_30 :: T_Dec_20 -> T_Reflects_16
d_proof_30 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2 -> T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2
T_Dec_20
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
d_From'45'yes_50 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_From'45'yes_50 :: () -> () -> T_Dec_20 -> ()
d_From'45'yes_50 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
d_From'45'no_52 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_From'45'no_52 :: () -> () -> T_Dec_20 -> ()
d_From'45'no_52 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
d_recompute_54 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> AgdaAny -> AgdaAny
d_recompute_54 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_recompute_54 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny -> AgdaAny
du_recompute_54 T_Dec_20
v2
du_recompute_54 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_recompute_54 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_recompute_54 T_Dec_20
v0 AgdaAny
v1
= (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_recompute_46
((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
d_recompute'45'constant_62 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
T_Dec_20 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_recompute'45'constant_62 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T__'8801'__12
d_recompute'45'constant_62 = () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T__'8801'__12
forall a. a
erased
d_T'63'_66 :: Bool -> T_Dec_20
d_T'63'_66 :: Bool -> T_Dec_20
d_T'63'_66 Bool
v0
= (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0)
((Bool -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.d_T'45'reflects_66 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
d_'172''63'_70 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> T_Dec_20
d_'172''63'_70 :: () -> () -> T_Dec_20 -> T_Dec_20
d_'172''63'_70 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> T_Dec_20
du_'172''63'_70 T_Dec_20
v2
du_'172''63'_70 :: T_Dec_20 -> T_Dec_20
du_'172''63'_70 :: T_Dec_20 -> T_Dec_20
du_'172''63'_70 T_Dec_20
v0
= (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0)))
((T_Reflects_16 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du_'172''45'reflects_70
((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0)))
d__'215''45'dec__76 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'215''45'dec__76 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'215''45'dec__76 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Dec_20
v4 T_Dec_20
v5
= T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__76 T_Dec_20
v4 T_Dec_20
v5
du__'215''45'dec__76 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__76 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'215''45'dec__76 T_Dec_20
v0 T_Dec_20
v1
= (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
((Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du__'215''45'reflects__82
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)) ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
d__'8846''45'dec__86 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8846''45'dec__86 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8846''45'dec__86 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Dec_20
v4 T_Dec_20
v5
= T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''45'dec__86 T_Dec_20
v4 T_Dec_20
v5
du__'8846''45'dec__86 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''45'dec__86 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8846''45'dec__86 T_Dec_20
v0 T_Dec_20
v1
= (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
((Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du__'8846''45'reflects__98
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)) ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
d__'8594''45'dec__96 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8594''45'dec__96 :: () -> () -> () -> () -> T_Dec_20 -> T_Dec_20 -> T_Dec_20
d__'8594''45'dec__96 ~()
v0 ~()
v1 ~()
v2 ~()
v3 T_Dec_20
v4 T_Dec_20
v5
= T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__96 T_Dec_20
v4 T_Dec_20
v5
du__'8594''45'dec__96 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__96 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du__'8594''45'dec__96 T_Dec_20
v0 T_Dec_20
v1
= (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0)))
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
((Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du__'8594''45'reflects__114
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)) ((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
((T_Dec_20 -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Reflects_16
d_proof_30 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v1)))
d_dec'8658'maybe_106 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> Maybe AgdaAny
d_dec'8658'maybe_106 :: () -> () -> T_Dec_20 -> Maybe AgdaAny
d_dec'8658'maybe_106 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 T_Dec_20
v2
du_dec'8658'maybe_106 :: T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 :: T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
else Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
T_Dec_20
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toSum_110 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_toSum_110 :: () -> () -> T_Dec_20 -> T__'8846'__30
d_toSum_110 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> T__'8846'__30
du_toSum_110 T_Dec_20
v2
du_toSum_110 ::
T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_toSum_110 :: T_Dec_20 -> T__'8846'__30
du_toSum_110 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
else (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
T_Dec_20
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromSum_116 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
d_fromSum_116 :: () -> () -> T__'8846'__30 -> T_Dec_20
d_fromSum_116 ~()
v0 ~()
v1 T__'8846'__30
v2 = T__'8846'__30 -> T_Dec_20
du_fromSum_116 T__'8846'__30
v2
du_fromSum_116 ::
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
du_fromSum_116 :: T__'8846'__30 -> T_Dec_20
du_fromSum_116 T__'8846'__30
v0
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v1
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v1
-> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8846'__30
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_isYes_122 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_isYes_122 :: () -> () -> T_Dec_20 -> Bool
d_isYes_122 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Bool
du_isYes_122 T_Dec_20
v2
du_isYes_122 :: T_Dec_20 -> Bool
du_isYes_122 :: T_Dec_20 -> Bool
du_isYes_122 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2 -> Bool -> Bool
forall a b. a -> b
coe Bool
v1
T_Dec_20
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
d_isNo_124 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_isNo_124 :: () -> () -> T_Dec_20 -> Bool
d_isNo_124 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> Bool
du_isNo_124 T_Dec_20
v2
du_isNo_124 :: T_Dec_20 -> Bool
du_isNo_124 :: T_Dec_20 -> Bool
du_isNo_124 T_Dec_20
v0
= (Bool -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
du_isYes_122 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
d_True_126 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_True_126 :: () -> () -> T_Dec_20 -> ()
d_True_126 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
d_False_128 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> ()
d_False_128 :: () -> () -> T_Dec_20 -> ()
d_False_128 = () -> () -> T_Dec_20 -> ()
forall a. a
erased
d_'8970'_'8971'_130 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> Bool
d_'8970'_'8971'_130 :: () -> () -> T_Dec_20 -> Bool
d_'8970'_'8971'_130 ()
v0 ()
v1 T_Dec_20
v2 = (T_Dec_20 -> Bool) -> T_Dec_20 -> Bool
forall a b. a -> b
coe T_Dec_20 -> Bool
du_isYes_122 T_Dec_20
v2
d_toWitness_134 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> AgdaAny -> AgdaAny
d_toWitness_134 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_toWitness_134 ~()
v0 ~()
v1 T_Dec_20
v2 ~AgdaAny
v3 = T_Dec_20 -> AgdaAny
du_toWitness_134 T_Dec_20
v2
du_toWitness_134 :: T_Dec_20 -> AgdaAny
du_toWitness_134 :: T_Dec_20 -> AgdaAny
du_toWitness_134 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v1)
((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromWitness_140 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> AgdaAny -> AgdaAny
d_fromWitness_140 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny
d_fromWitness_140 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_140 T_Dec_20
v2
du_fromWitness_140 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_140 :: T_Dec_20 -> AgdaAny -> AgdaAny
du_fromWitness_140 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then let v3 :: b
v3 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
forall a. a
v3))
else (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
T_Dec_20
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_toWitnessFalse_146 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
T_Dec_20 ->
AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_toWitnessFalse_146 :: () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_Irrelevant_20
d_toWitnessFalse_146 = () -> () -> T_Dec_20 -> AgdaAny -> AgdaAny -> T_Irrelevant_20
forall a. a
erased
d_fromWitnessFalse_152 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
T_Dec_20 ->
(AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
AgdaAny
d_fromWitnessFalse_152 :: () -> () -> T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
d_fromWitnessFalse_152 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_fromWitnessFalse_152 T_Dec_20
v2
du_fromWitnessFalse_152 ::
T_Dec_20 ->
(AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
AgdaAny
du_fromWitnessFalse_152 :: T_Dec_20 -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_fromWitnessFalse_152 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (AgdaAny -> AgdaAny) -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v3 ->
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
v3
((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)))
else (let v3 :: b
v3 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
AgdaAny -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
forall a b. a -> b
coe ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
forall a. a
v3)))
T_Dec_20
_ -> (AgdaAny -> T_Irrelevant_20) -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_from'45'yes_158 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> AgdaAny
d_from'45'yes_158 :: () -> () -> T_Dec_20 -> AgdaAny
d_from'45'yes_158 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny
du_from'45'yes_158 T_Dec_20
v2
du_from'45'yes_158 :: T_Dec_20 -> AgdaAny
du_from'45'yes_158 :: T_Dec_20 -> AgdaAny
du_from'45'yes_158 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
else (AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
(() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_from'45'no_164 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> T_Dec_20 -> AgdaAny
d_from'45'no_164 :: () -> () -> T_Dec_20 -> AgdaAny
d_from'45'no_164 ~()
v0 ~()
v1 T_Dec_20
v2 = T_Dec_20 -> AgdaAny
du_from'45'no_164 T_Dec_20
v2
du_from'45'no_164 :: T_Dec_20 -> AgdaAny
du_from'45'no_164 :: T_Dec_20 -> AgdaAny
du_from'45'no_164 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
(() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
else (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_map'8242'_168 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
d_map'8242'_168 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Dec_20
-> T_Dec_20
d_map'8242'_168 ~()
v0 ~()
v1 ~()
v2 ~()
v3 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 T_Dec_20
v6
= (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 AgdaAny -> AgdaAny
v4 AgdaAny -> AgdaAny
v5 T_Dec_20
v6
du_map'8242'_168 ::
(AgdaAny -> AgdaAny) ->
(AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 :: (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny
v1 T_Dec_20
v2
= (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
C__because__32 ((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v2))
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 of
C__because__32 Bool
v3 T_Reflects_16
v4
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
then (Bool -> AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du_of_30
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v2)))
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny -> AgdaAny
v0
((T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v4)))
else (Bool -> AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.du_of_30
((T_Dec_20 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Bool
d_does_28 (((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v2)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v5 ->
(T_Reflects_16 -> AgdaAny) -> T_Reflects_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 T_Reflects_16
v4
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v5)))
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_decidable'45'stable_188 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
T_Dec_20 ->
((AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
AgdaAny
d_decidable'45'stable_188 :: ()
-> ()
-> T_Dec_20
-> ((AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20)
-> AgdaAny
d_decidable'45'stable_188 ~()
v0 ~()
v1 T_Dec_20
v2 ~(AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20
v3
= T_Dec_20 -> AgdaAny
du_decidable'45'stable_188 T_Dec_20
v2
du_decidable'45'stable_188 :: T_Dec_20 -> AgdaAny
du_decidable'45'stable_188 :: T_Dec_20 -> AgdaAny
du_decidable'45'stable_188 T_Dec_20
v0
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 of
C__because__32 Bool
v1 T_Reflects_16
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (T_Reflects_16 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Reflects.du_invert_38 (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v2)
else ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
AgdaAny
forall a. a
erased
T_Dec_20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'172''45'drop'45'Dec_198 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> T_Dec_20
d_'172''45'drop'45'Dec_198 :: () -> () -> T_Dec_20 -> T_Dec_20
d_'172''45'drop'45'Dec_198 ~()
v0 ~()
v1 T_Dec_20
v2
= T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_198 T_Dec_20
v2
du_'172''45'drop'45'Dec_198 :: T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_198 :: T_Dec_20 -> T_Dec_20
du_'172''45'drop'45'Dec_198 T_Dec_20
v0
= ((AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
(AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_map'8242'_168 AgdaAny
forall a. a
erased
(\ AgdaAny
v1 ->
((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44)
((T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Dec_20
du_'172''63'_70 (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v0))
d_'172''172''45'excluded'45'middle_202 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(T_Dec_20 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'172''172''45'excluded'45'middle_202 :: () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
d_'172''172''45'excluded'45'middle_202 = () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
forall a. a
erased
d_excluded'45'middle_208 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(T_Dec_20 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_excluded'45'middle_208 :: () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
d_excluded'45'middle_208 = () -> () -> (T_Dec_20 -> T_Irrelevant_20) -> T_Irrelevant_20
forall a. a
erased
d_decToMaybe_210 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> Maybe AgdaAny
d_decToMaybe_210 :: () -> () -> T_Dec_20 -> Maybe AgdaAny
d_decToMaybe_210 ()
v0 ()
v1 T_Dec_20
v2 = (T_Dec_20 -> Maybe AgdaAny) -> T_Dec_20 -> Maybe AgdaAny
forall a b. a -> b
coe T_Dec_20 -> Maybe AgdaAny
du_dec'8658'maybe_106 T_Dec_20
v2
d_fromDec_212 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_20 -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_fromDec_212 :: () -> () -> T_Dec_20 -> T__'8846'__30
d_fromDec_212 ()
v0 ()
v1 T_Dec_20
v2 = (T_Dec_20 -> T__'8846'__30) -> T_Dec_20 -> T__'8846'__30
forall a b. a -> b
coe T_Dec_20 -> T__'8846'__30
du_toSum_110 T_Dec_20
v2
d_toDec_214 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> T_Dec_20
d_toDec_214 :: () -> () -> T__'8846'__30 -> T_Dec_20
d_toDec_214 ()
v0 ()
v1 T__'8846'__30
v2 = (T__'8846'__30 -> T_Dec_20) -> T__'8846'__30 -> T_Dec_20
forall a b. a -> b
coe T__'8846'__30 -> T_Dec_20
du_fromSum_116 T__'8846'__30
v2