{-# 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.Product 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Relation.Nullary

-- Relation.Nullary.Product._×-reflects_
d__'215''45'reflects__18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Relation.Nullary.T_Reflects_14
d__'215''45'reflects__18 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> Bool
-> Bool
-> T_Reflects_14
-> T_Reflects_14
-> T_Reflects_14
d__'215''45'reflects__18 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~Bool
v4 ~Bool
v5 T_Reflects_14
v6 T_Reflects_14
v7
  = T_Reflects_14 -> T_Reflects_14 -> T_Reflects_14
du__'215''45'reflects__18 T_Reflects_14
v6 T_Reflects_14
v7
du__'215''45'reflects__18 ::
  MAlonzo.Code.Relation.Nullary.T_Reflects_14 ->
  MAlonzo.Code.Relation.Nullary.T_Reflects_14 ->
  MAlonzo.Code.Relation.Nullary.T_Reflects_14
du__'215''45'reflects__18 :: T_Reflects_14 -> T_Reflects_14 -> T_Reflects_14
du__'215''45'reflects__18 T_Reflects_14
v0 T_Reflects_14
v1
  = 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
v2
        -> case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v1 of
             MAlonzo.Code.Relation.Nullary.C_of'696'_22 AgdaAny
v3
               -> (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 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
             T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
               -> T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
             T_Reflects_14
_ -> T_Reflects_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
        -> T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
      T_Reflects_14
_ -> T_Reflects_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Product._×-dec_
d__'215''45'dec__30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'215''45'dec__30 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Dec_32
-> T_Dec_32
-> T_Dec_32
d__'215''45'dec__30 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Dec_32
v4 T_Dec_32
v5
  = T_Dec_32 -> T_Dec_32 -> T_Dec_32
du__'215''45'dec__30 T_Dec_32
v4 T_Dec_32
v5
du__'215''45'dec__30 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'215''45'dec__30 :: T_Dec_32 -> T_Dec_32 -> T_Dec_32
du__'215''45'dec__30 T_Dec_32
v0 T_Dec_32
v1
  = (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 -> Bool -> Bool) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
         ((T_Dec_32 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> Bool
MAlonzo.Code.Relation.Nullary.d_does_42 (T_Dec_32 -> AgdaAny
forall a b. a -> b
coe T_Dec_32
v0))
         ((T_Dec_32 -> Bool) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> Bool
MAlonzo.Code.Relation.Nullary.d_does_42 (T_Dec_32 -> AgdaAny
forall a b. a -> b
coe T_Dec_32
v1)))
      ((T_Reflects_14 -> T_Reflects_14 -> T_Reflects_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Reflects_14 -> T_Reflects_14 -> T_Reflects_14
du__'215''45'reflects__18
         ((T_Dec_32 -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.d_proof_44 (T_Dec_32 -> AgdaAny
forall a b. a -> b
coe T_Dec_32
v0))
         ((T_Dec_32 -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.d_proof_44 (T_Dec_32 -> AgdaAny
forall a b. a -> b
coe T_Dec_32
v1)))