{-# 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.Reflection.AST.Argument.Modality 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.Reflection
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Reflection.AST.Argument.QQuantity
import qualified MAlonzo.Code.Reflection.AST.Argument.Relevance
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Reflection.AST.Argument.Modality.relevance
d_relevance_16 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56
d_relevance_16 :: T_Modality_68 -> T_Relevance_56
d_relevance_16 T_Modality_68
v0
  = case T_Modality_68 -> T_Modality_68
forall a b. a -> b
coe T_Modality_68
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 T_Relevance_56
v1 T_Quantity_62
v2 -> T_Relevance_56 -> T_Relevance_56
forall a b. a -> b
coe T_Relevance_56
v1
      T_Modality_68
_ -> T_Relevance_56
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Argument.Modality.quantity
d_quantity_20 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62
d_quantity_20 :: T_Modality_68 -> T_Quantity_62
d_quantity_20 T_Modality_68
v0
  = case T_Modality_68 -> T_Modality_68
forall a b. a -> b
coe T_Modality_68
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 T_Relevance_56
v1 T_Quantity_62
v2 -> T_Quantity_62 -> T_Quantity_62
forall a b. a -> b
coe T_Quantity_62
v2
      T_Modality_68
_ -> T_Quantity_62
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Argument.Modality.modality-injective₁
d_modality'45'injective'8321'_24 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_modality'45'injective'8321'_24 :: T_Relevance_56
-> T_Quantity_62
-> T_Relevance_56
-> T_Quantity_62
-> T__'8801'__12
-> T__'8801'__12
d_modality'45'injective'8321'_24 = T_Relevance_56
-> T_Quantity_62
-> T_Relevance_56
-> T_Quantity_62
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Argument.Modality.modality-injective₂
d_modality'45'injective'8322'_26 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_modality'45'injective'8322'_26 :: T_Relevance_56
-> T_Quantity_62
-> T_Relevance_56
-> T_Quantity_62
-> T__'8801'__12
-> T__'8801'__12
d_modality'45'injective'8322'_26 = T_Relevance_56
-> T_Quantity_62
-> T_Relevance_56
-> T_Quantity_62
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Argument.Modality.modality-injective
d_modality'45'injective_28 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_modality'45'injective_28 :: T_Relevance_56
-> T_Quantity_62
-> T_Relevance_56
-> T_Quantity_62
-> T__'8801'__12
-> T_Σ_14
d_modality'45'injective_28 ~T_Relevance_56
v0 ~T_Quantity_62
v1 ~T_Relevance_56
v2 ~T_Quantity_62
v3
  = T__'8801'__12 -> T_Σ_14
du_modality'45'injective_28
du_modality'45'injective_28 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_modality'45'injective_28 :: T__'8801'__12 -> T_Σ_14
du_modality'45'injective_28
  = ((Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14)
-> Any -> Any -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 Any
forall a. a
erased Any
forall a. a
erased
-- Reflection.AST.Argument.Modality._≟_
d__'8799'__30 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__30 :: T_Modality_68 -> T_Modality_68 -> T_Dec_20
d__'8799'__30 T_Modality_68
v0 T_Modality_68
v1
  = case T_Modality_68 -> T_Modality_68
forall a b. a -> b
coe T_Modality_68
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 T_Relevance_56
v2 T_Quantity_62
v3
        -> case T_Modality_68 -> T_Modality_68
forall a b. a -> b
coe T_Modality_68
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 T_Relevance_56
v4 T_Quantity_62
v5
               -> ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
                    (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((Any -> Any -> Any) -> T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe (Any -> Any -> Any) -> T_Σ_14 -> Any
MAlonzo.Code.Data.Product.Base.du_uncurry_244 Any
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> Any
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_modality'45'injective_28)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((T_Relevance_56 -> T_Relevance_56 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Relevance_56 -> T_Relevance_56 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.Relevance.d__'8799'__8
                          (T_Relevance_56 -> Any
forall a b. a -> b
coe T_Relevance_56
v2) (T_Relevance_56 -> Any
forall a b. a -> b
coe T_Relevance_56
v4))
                       ((T_Quantity_62 -> T_Quantity_62 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Quantity_62 -> T_Quantity_62 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.QQuantity.d__'8799'__8
                          (T_Quantity_62 -> Any
forall a b. a -> b
coe T_Quantity_62
v3) (T_Quantity_62 -> Any
forall a b. a -> b
coe T_Quantity_62
v5)))
             T_Modality_68
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Modality_68
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError