{-# 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.Reflects where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.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.Relation.Nullary.Negation.Core
d_Reflects_16 :: p -> p -> p -> ()
d_Reflects_16 p
a0 p
a1 p
a2 = ()
data T_Reflects_16 = C_of'696'_22 AgdaAny | C_of'8319'_26
d_of_30 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Bool -> AgdaAny -> T_Reflects_16
d_of_30 :: () -> () -> Bool -> AgdaAny -> T_Reflects_16
d_of_30 ~()
v0 ~()
v1 Bool
v2 AgdaAny
v3 = Bool -> AgdaAny -> T_Reflects_16
du_of_30 Bool
v2 AgdaAny
v3
du_of_30 :: Bool -> AgdaAny -> T_Reflects_16
du_of_30 :: Bool -> AgdaAny -> T_Reflects_16
du_of_30 Bool
v0 AgdaAny
v1
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0 then (AgdaAny -> T_Reflects_16) -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) else T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
C_of'8319'_26
d_invert_38 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Bool -> T_Reflects_16 -> AgdaAny
d_invert_38 :: () -> () -> Bool -> T_Reflects_16 -> AgdaAny
d_invert_38 ~()
v0 ~()
v1 ~Bool
v2 T_Reflects_16
v3 = T_Reflects_16 -> AgdaAny
du_invert_38 T_Reflects_16
v3
du_invert_38 :: T_Reflects_16 -> AgdaAny
du_invert_38 :: T_Reflects_16 -> AgdaAny
du_invert_38 T_Reflects_16
v0
= case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v0 of
C_of'696'_22 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
T_Reflects_16
C_of'8319'_26 -> AgdaAny
forall a. a
erased
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_recompute_46 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Bool -> T_Reflects_16 -> AgdaAny -> AgdaAny
d_recompute_46 :: () -> () -> Bool -> T_Reflects_16 -> AgdaAny -> AgdaAny
d_recompute_46 ~()
v0 ~()
v1 ~Bool
v2 T_Reflects_16
v3 ~AgdaAny
v4 = T_Reflects_16 -> AgdaAny
du_recompute_46 T_Reflects_16
v3
du_recompute_46 :: T_Reflects_16 -> AgdaAny
du_recompute_46 :: T_Reflects_16 -> AgdaAny
du_recompute_46 T_Reflects_16
v0
= case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v0 of
C_of'696'_22 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
T_Reflects_16
C_of'8319'_26
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction'45'irr_38
T_Reflects_16
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_recompute'45'constant_62 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Bool ->
T_Reflects_16 ->
AgdaAny ->
AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_recompute'45'constant_62 :: ()
-> ()
-> Bool
-> T_Reflects_16
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
d_recompute'45'constant_62 = ()
-> ()
-> Bool
-> T_Reflects_16
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
forall a. a
erased
d_T'45'reflects_66 :: Bool -> T_Reflects_16
d_T'45'reflects_66 :: Bool -> T_Reflects_16
d_T'45'reflects_66 Bool
v0
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0) (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
else (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
d_'172''45'reflects_70 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> Bool -> T_Reflects_16 -> T_Reflects_16
d_'172''45'reflects_70 :: () -> () -> Bool -> T_Reflects_16 -> T_Reflects_16
d_'172''45'reflects_70 ~()
v0 ~()
v1 ~Bool
v2 T_Reflects_16
v3 = T_Reflects_16 -> T_Reflects_16
du_'172''45'reflects_70 T_Reflects_16
v3
du_'172''45'reflects_70 :: T_Reflects_16 -> T_Reflects_16
du_'172''45'reflects_70 :: T_Reflects_16 -> T_Reflects_16
du_'172''45'reflects_70 T_Reflects_16
v0
= case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v0 of
C_of'696'_22 AgdaAny
v1
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2 AgdaAny
v1))
T_Reflects_16
C_of'8319'_26
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
AgdaAny
forall a. a
erased
T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'215''45'reflects__82 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Bool -> Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
d__'215''45'reflects__82 :: ()
-> ()
-> ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T_Reflects_16
d__'215''45'reflects__82 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Bool
v4 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
= Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'215''45'reflects__82 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
du__'215''45'reflects__82 ::
Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'215''45'reflects__82 :: Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'215''45'reflects__82 Bool
v0 T_Reflects_16
v1 T_Reflects_16
v2
= case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v1 of
C_of'696'_22 AgdaAny
v3
-> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
C_of'696'_22 AgdaAny
v4
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
T_Reflects_16
C_of'8319'_26
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
AgdaAny
forall a. a
erased
T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
C_of'8319'_26
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
AgdaAny
forall a. a
erased
T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8846''45'reflects__98 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Bool -> Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
d__'8846''45'reflects__98 :: ()
-> ()
-> ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T_Reflects_16
d__'8846''45'reflects__98 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Bool
v4 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
= Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8846''45'reflects__98 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
du__'8846''45'reflects__98 ::
Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8846''45'reflects__98 :: Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8846''45'reflects__98 Bool
v0 T_Reflects_16
v1 T_Reflects_16
v2
= case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v1 of
C_of'696'_22 AgdaAny
v3
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10) (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
T_Reflects_16
C_of'8319'_26
-> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
C_of'696'_22 AgdaAny
v4
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
T_Reflects_16
C_of'8319'_26
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((Bool -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8744'__30
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
AgdaAny
forall a. a
erased
T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
d__'8594''45'reflects__114 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Bool -> Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
d__'8594''45'reflects__114 :: ()
-> ()
-> ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T_Reflects_16
d__'8594''45'reflects__114 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~Bool
v4 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
= Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8594''45'reflects__114 Bool
v5 T_Reflects_16
v6 T_Reflects_16
v7
du__'8594''45'reflects__114 ::
Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8594''45'reflects__114 :: Bool -> T_Reflects_16 -> T_Reflects_16 -> T_Reflects_16
du__'8594''45'reflects__114 Bool
v0 T_Reflects_16
v1 T_Reflects_16
v2
= case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v1 of
C_of'696'_22 AgdaAny
v3
-> case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v2 of
C_of'696'_22 AgdaAny
v4
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((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
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 -> AgdaAny
v4))
T_Reflects_16
C_of'8319'_26
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((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
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10))
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
AgdaAny
forall a. a
erased
T_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
C_of'8319'_26
-> (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30
((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
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8))
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
(\ AgdaAny
v4 ->
((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_Reflects_16
_ -> T_Reflects_16
forall a. a
MAlonzo.RTE.mazUnreachableError
d_fromEquivalence_132 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Bool ->
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
d_fromEquivalence_132 :: ()
-> ()
-> Bool
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Reflects_16
d_fromEquivalence_132 ~()
v0 ~()
v1 Bool
v2 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
= Bool
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
du_fromEquivalence_132 Bool
v2 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny
v4
du_fromEquivalence_132 ::
Bool ->
(AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
du_fromEquivalence_132 :: Bool
-> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Reflects_16
du_fromEquivalence_132 Bool
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2
= if Bool -> Bool
forall a b. a -> b
coe Bool
v0
then (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe
Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0)
((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
else (Bool -> AgdaAny -> T_Reflects_16)
-> AgdaAny -> AgdaAny -> T_Reflects_16
forall a b. a -> b
coe Bool -> AgdaAny -> T_Reflects_16
du_of_30 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2)
d_det_146 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
Bool ->
Bool ->
T_Reflects_16 ->
T_Reflects_16 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_det_146 :: ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T__'8801'__12
d_det_146 = ()
-> ()
-> Bool
-> Bool
-> T_Reflects_16
-> T_Reflects_16
-> T__'8801'__12
forall a. a
erased
d_T'45'reflects'45'elim_164 ::
Bool ->
Bool ->
T_Reflects_16 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_T'45'reflects'45'elim_164 :: Bool -> Bool -> T_Reflects_16 -> T__'8801'__12
d_T'45'reflects'45'elim_164 = Bool -> Bool -> T_Reflects_16 -> T__'8801'__12
forall a. a
erased