{-# 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.Utils.Decidable where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
d_dmap_12 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny) ->
((AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dmap_12 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny -> T_Irrelevant_20)
-> T_Dec_20
-> T_Dec_20
d_dmap_12 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~(AgdaAny -> T_Irrelevant_20) -> AgdaAny -> T_Irrelevant_20
v5 T_Dec_20
v6 = (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_dmap_12 AgdaAny -> AgdaAny
v4 T_Dec_20
v6
du_dmap_12 ::
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dmap_12 :: (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_dmap_12 AgdaAny -> AgdaAny
v0 T_Dec_20
v1
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
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 AgdaAny
v4
-> (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
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
((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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4))
T_Reflects_16
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
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
v3)
((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
v2)
(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
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_dcong_40 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny) ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dcong_40 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T__'8801'__12)
-> T_Dec_20
-> T_Dec_20
d_dcong_40 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~AgdaAny -> AgdaAny
v6 ~T__'8801'__12 -> T__'8801'__12
v7 = T_Dec_20 -> T_Dec_20
du_dcong_40
du_dcong_40 ::
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dcong_40 :: T_Dec_20 -> T_Dec_20
du_dcong_40 = ((AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
du_dmap_12 AgdaAny
forall a. a
erased
d_dcong'8322'_70 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
() ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dcong'8322'_70 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T_Σ_14)
-> T_Dec_20
-> T_Dec_20
-> T_Dec_20
d_dcong'8322'_70 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9 ~AgdaAny -> AgdaAny -> AgdaAny
v10 ~T__'8801'__12 -> T_Σ_14
v11
T_Dec_20
v12 T_Dec_20
v13
= T_Dec_20 -> T_Dec_20 -> T_Dec_20
du_dcong'8322'_70 T_Dec_20
v12 T_Dec_20
v13
du_dcong'8322'_70 ::
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dcong'8322'_70 :: T_Dec_20 -> T_Dec_20 -> T_Dec_20
du_dcong'8322'_70 T_Dec_20
v0 T_Dec_20
v1
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v0 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 (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
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
v3)
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 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
-> (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)
((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
forall a. a
erased)
T_Reflects_16
_ -> (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
v4)
((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_false_8)
(T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)))
else (case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26
-> (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_Reflects_16
_ -> (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
v4)
((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)
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
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
v3)
((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
v2)
(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
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_dhcong_120 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
() ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny) ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
(AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dhcong_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T_Σ_14)
-> T_Dec_20
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
d_dhcong_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny
v6 ~AgdaAny
v7 ~AgdaAny
v8 AgdaAny
v9 ~AgdaAny -> AgdaAny -> AgdaAny
v10 ~T__'8801'__12 -> T_Σ_14
v11 T_Dec_20
v12
AgdaAny -> T_Dec_20
v13
= AgdaAny -> T_Dec_20 -> (AgdaAny -> T_Dec_20) -> T_Dec_20
du_dhcong_120 AgdaAny
v9 T_Dec_20
v12 AgdaAny -> T_Dec_20
v13
du_dhcong_120 ::
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
(AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dhcong_120 :: AgdaAny -> T_Dec_20 -> (AgdaAny -> T_Dec_20) -> T_Dec_20
du_dhcong_120 AgdaAny
v0 T_Dec_20
v1 AgdaAny -> T_Dec_20
v2
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 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 (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
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
v4) ((T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_20 -> T_Dec_20
du_dcong_40 ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v2 AgdaAny
v0))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
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
v4)
((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
v3)
(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
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_dhcong'8322'_180 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
(AgdaAny -> ()) ->
(AgdaAny -> ()) ->
() ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
AgdaAny ->
(AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
(MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
(AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_dhcong'8322'_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (T__'8801'__12 -> T_Σ_14)
-> T_Dec_20
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
d_dhcong'8322'_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9 AgdaAny
v10 ~AgdaAny
v11
AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~T__'8801'__12 -> T_Σ_14
v14 T_Dec_20
v15 AgdaAny -> T_Dec_20
v16 AgdaAny -> T_Dec_20
v17
= AgdaAny
-> AgdaAny
-> T_Dec_20
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
du_dhcong'8322'_180 AgdaAny
v10 AgdaAny
v12 T_Dec_20
v15 AgdaAny -> T_Dec_20
v16 AgdaAny -> T_Dec_20
v17
du_dhcong'8322'_180 ::
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
(AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
(AgdaAny ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_dhcong'8322'_180 :: AgdaAny
-> AgdaAny
-> T_Dec_20
-> (AgdaAny -> T_Dec_20)
-> (AgdaAny -> T_Dec_20)
-> T_Dec_20
du_dhcong'8322'_180 AgdaAny
v0 AgdaAny
v1 T_Dec_20
v2 AgdaAny -> T_Dec_20
v3 AgdaAny -> T_Dec_20
v4
= case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 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 -> T_Dec_20
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_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
du_dcong'8322'_70 ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v3 AgdaAny
v0) ((AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_20
v4 AgdaAny
v1))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_20
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)
((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
v5)
(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
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError