{-# 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.Empty
import qualified MAlonzo.Code.Relation.Nullary
d_dmap_12 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
() ->
(AgdaAny -> AgdaAny) ->
((AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dmap_12 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> ((AgdaAny -> T_'8869'_4) -> AgdaAny -> T_'8869'_4)
-> T_Dec_32
-> T_Dec_32
d_dmap_12 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 ~(AgdaAny -> T_'8869'_4) -> AgdaAny -> T_'8869'_4
v5 T_Dec_32
v6 = (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
du_dmap_12 AgdaAny -> AgdaAny
v4 T_Dec_32
v6
du_dmap_12 ::
(AgdaAny -> AgdaAny) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dmap_12 :: (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
du_dmap_12 AgdaAny -> AgdaAny
v0 T_Dec_32
v1
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v1 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v2 T_Reflects_14
v3
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v3 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v4
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v4))
T_Reflects_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v3)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> T_Dec_32
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.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
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_32
-> T_Dec_32
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_32 -> T_Dec_32
du_dcong_40
du_dcong_40 ::
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dcong_40 :: T_Dec_32 -> T_Dec_32
du_dcong_40 = ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
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.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
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_32
-> T_Dec_32
-> T_Dec_32
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_32
v12 T_Dec_32
v13
= T_Dec_32 -> T_Dec_32 -> T_Dec_32
du_dcong'8322'_70 T_Dec_32
v12 T_Dec_32
v13
du_dcong'8322'_70 ::
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dcong'8322'_70 :: T_Dec_32 -> T_Dec_32 -> T_Dec_32
du_dcong'8322'_70 T_Dec_32
v0 T_Dec_32
v1
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v2 T_Reflects_14
v3
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v3)
(case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v1 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v4 T_Reflects_14
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v5 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v6
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
forall a. a
erased)
T_Reflects_14
_ -> (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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v5)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)))
else (case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v5 of
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
-> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
T_Reflects_14
_ -> (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_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v5)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> AgdaAny
forall a b. a -> b
coe Bool
v4)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))))
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v3)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v2)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> T_Dec_32
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.T_Dec_32 ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
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_32
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
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_32
v12
AgdaAny -> T_Dec_32
v13
= AgdaAny -> T_Dec_32 -> (AgdaAny -> T_Dec_32) -> T_Dec_32
du_dhcong_120 AgdaAny
v9 T_Dec_32
v12 AgdaAny -> T_Dec_32
v13
du_dhcong_120 ::
AgdaAny ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dhcong_120 :: AgdaAny -> T_Dec_32 -> (AgdaAny -> T_Dec_32) -> T_Dec_32
du_dhcong_120 AgdaAny
v0 T_Dec_32
v1 AgdaAny -> T_Dec_32
v2
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v1 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v3 T_Reflects_14
v4
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v4) ((T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> T_Dec_32
du_dcong_40 ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v2 AgdaAny
v0))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v4)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v3)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> T_Dec_32
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.T_Dec_32 ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
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_32
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
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_32
v15 AgdaAny -> T_Dec_32
v16 AgdaAny -> T_Dec_32
v17
= AgdaAny
-> AgdaAny
-> T_Dec_32
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
du_dhcong'8322'_180 AgdaAny
v10 AgdaAny
v12 T_Dec_32
v15 AgdaAny -> T_Dec_32
v16 AgdaAny -> T_Dec_32
v17
du_dhcong'8322'_180 ::
AgdaAny ->
AgdaAny ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
(AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dhcong'8322'_180 :: AgdaAny
-> AgdaAny
-> T_Dec_32
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Dec_32
du_dhcong'8322'_180 AgdaAny
v0 AgdaAny
v1 T_Dec_32
v2 AgdaAny -> T_Dec_32
v3 AgdaAny -> T_Dec_32
v4
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v2 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v5 T_Reflects_14
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v6) ((T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> T_Dec_32 -> T_Dec_32
du_dcong'8322'_70 ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v3 AgdaAny
v0) ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v4 AgdaAny
v1))
else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
v6)
((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> AgdaAny
forall a b. a -> b
coe Bool
v5)
(T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError