{-# 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 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.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Empty.Irrelevant
d_'172'__6 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_'172'__6 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_'172'__6 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
d_Reflects_14 :: p -> p -> p -> T_Level_18
d_Reflects_14 p
a0 p
a1 p
a2 = ()
data T_Reflects_14 = C_of'696'_22 AgdaAny | C_of'8319'_26
d_Dec_32 :: p -> p -> T_Level_18
d_Dec_32 p
a0 p
a1 = ()
data T_Dec_32 = C__because__46 Bool T_Reflects_14
d_does_42 :: T_Dec_32 -> Bool
d_does_42 :: T_Dec_32 -> Bool
d_does_42 T_Dec_32
v0
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
C__because__46 Bool
v1 T_Reflects_14
v2 -> Bool -> Bool
forall a b. a -> b
coe Bool
v1
T_Dec_32
_ -> Bool
forall a. a
MAlonzo.RTE.mazUnreachableError
d_proof_44 :: T_Dec_32 -> T_Reflects_14
d_proof_44 :: T_Dec_32 -> T_Reflects_14
d_proof_44 T_Dec_32
v0
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
C__because__46 Bool
v1 T_Reflects_14
v2 -> T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v2
T_Dec_32
_ -> T_Reflects_14
forall a. a
MAlonzo.RTE.mazUnreachableError
d_recompute_60 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() -> T_Dec_32 -> AgdaAny -> AgdaAny
d_recompute_60 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> AgdaAny -> AgdaAny
d_recompute_60 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 ~AgdaAny
v3 = T_Dec_32 -> AgdaAny
du_recompute_60 T_Dec_32
v2
du_recompute_60 :: T_Dec_32 -> AgdaAny
du_recompute_60 :: T_Dec_32 -> AgdaAny
du_recompute_60 T_Dec_32
v0
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v0 of
C__because__46 Bool
v1 T_Reflects_14
v2
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v2 of
C_of'696'_22 AgdaAny
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3
T_Reflects_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
else (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
v2)
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Irrelevant.du_'8869''45'elim_10)
T_Dec_32
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Irrelevant_70 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_Irrelevant_70 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_Irrelevant_70 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased