{-# 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

-- Relation.Nullary.¬_
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
-- Relation.Nullary.Reflects
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
-- Relation.Nullary.Dec
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
-- Relation.Nullary.Dec.does
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
-- Relation.Nullary.Dec.proof
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
-- Relation.Nullary.recompute
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
-- Relation.Nullary.Irrelevant
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