{-# 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Relation.Nullary

-- Relation.Nullary.Reflects.of
d_of_12 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Reflects_14
d_of_12 :: T_Level_18 -> T_Level_18 -> Bool -> AgdaAny -> T_Reflects_14
d_of_12 ~T_Level_18
v0 ~T_Level_18
v1 Bool
v2 AgdaAny
v3 = Bool -> AgdaAny -> T_Reflects_14
du_of_12 Bool
v2 AgdaAny
v3
du_of_12 ::
  Bool -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Reflects_14
du_of_12 :: Bool -> AgdaAny -> T_Reflects_14
du_of_12 Bool
v0 AgdaAny
v1
  = if Bool -> Bool
forall a b. a -> b
coe Bool
v0
      then (AgdaAny -> T_Reflects_14) -> AgdaAny -> T_Reflects_14
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
      else T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
-- Relation.Nullary.Reflects.invert
d_invert_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool -> MAlonzo.Code.Relation.Nullary.T_Reflects_14 -> AgdaAny
d_invert_20 :: T_Level_18 -> T_Level_18 -> Bool -> T_Reflects_14 -> AgdaAny
d_invert_20 ~T_Level_18
v0 ~T_Level_18
v1 ~Bool
v2 T_Reflects_14
v3 = T_Reflects_14 -> AgdaAny
du_invert_20 T_Reflects_14
v3
du_invert_20 ::
  MAlonzo.Code.Relation.Nullary.T_Reflects_14 -> AgdaAny
du_invert_20 :: T_Reflects_14 -> AgdaAny
du_invert_20 T_Reflects_14
v0
  = case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v0 of
      MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v1 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26 -> AgdaAny
forall a. a
erased
      T_Reflects_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Reflects.fromEquivalence
d_fromEquivalence_28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Relation.Nullary.T_Reflects_14
d_fromEquivalence_28 :: T_Level_18
-> T_Level_18
-> Bool
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> T_Reflects_14
d_fromEquivalence_28 ~T_Level_18
v0 ~T_Level_18
v1 Bool
v2 AgdaAny -> AgdaAny
v3 ~AgdaAny -> AgdaAny
v4
  = Bool -> (AgdaAny -> AgdaAny) -> T_Reflects_14
du_fromEquivalence_28 Bool
v2 AgdaAny -> AgdaAny
v3
du_fromEquivalence_28 ::
  Bool ->
  (AgdaAny -> AgdaAny) -> MAlonzo.Code.Relation.Nullary.T_Reflects_14
du_fromEquivalence_28 :: Bool -> (AgdaAny -> AgdaAny) -> T_Reflects_14
du_fromEquivalence_28 Bool
v0 AgdaAny -> AgdaAny
v1
  = if Bool -> Bool
forall a b. a -> b
coe Bool
v0
      then (AgdaAny -> T_Reflects_14) -> AgdaAny -> T_Reflects_14
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
v1 (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
      else T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
-- Relation.Nullary.Reflects.det
d_det_42 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool ->
  Bool ->
  MAlonzo.Code.Relation.Nullary.T_Reflects_14 ->
  MAlonzo.Code.Relation.Nullary.T_Reflects_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_det_42 :: T_Level_18
-> T_Level_18
-> Bool
-> Bool
-> T_Reflects_14
-> T_Reflects_14
-> T__'8801'__12
d_det_42 = T_Level_18
-> T_Level_18
-> Bool
-> Bool
-> T_Reflects_14
-> T_Reflects_14
-> T__'8801'__12
forall a. a
erased