{-# 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.Negation 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.Irrelevant
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Effect.Monad
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Nullary.Negation.∃⟶¬∀¬
d_'8707''10230''172''8704''172'_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8707''10230''172''8704''172'_32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
d_'8707''10230''172''8704''172'_32 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.∀⟶¬∃¬
d_'8704''10230''172''8707''172'_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8704''10230''172''8707''172'_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Irrelevant_20
d_'8704''10230''172''8707''172'_38 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.¬∃⟶∀¬
d_'172''8707''10230''8704''172'_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'172''8707''10230''8704''172'_50 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (T_Σ_14 -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_'172''8707''10230''8704''172'_50 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (T_Σ_14 -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.∀¬⟶¬∃
d_'8704''172''10230''172''8707'_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8704''172''10230''172''8707'_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Irrelevant_20
d_'8704''172''10230''172''8707'_56 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> T_Σ_14
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.∃¬⟶¬∀
d_'8707''172''10230''172''8704'_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'8707''172''10230''172''8704'_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> T_Irrelevant_20
d_'8707''172''10230''172''8704'_62 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.¬¬-Monad
d_'172''172''45'Monad_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Effect.Monad.T_RawMonad_24
d_'172''172''45'Monad_64 :: T_Level_18 -> T_RawMonad_24
d_'172''172''45'Monad_64 ~T_Level_18
v0 = T_RawMonad_24
du_'172''172''45'Monad_64
du_'172''172''45'Monad_64 ::
  MAlonzo.Code.Effect.Monad.T_RawMonad_24
du_'172''172''45'Monad_64 :: T_RawMonad_24
du_'172''172''45'Monad_64
  = ((T_Level_18 -> AgdaAny -> AgdaAny)
 -> (T_Level_18
     -> T_Level_18 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
 -> T_RawMonad_24)
-> AgdaAny -> AgdaAny -> T_RawMonad_24
forall a b. a -> b
coe
      (T_Level_18 -> AgdaAny -> AgdaAny)
-> (T_Level_18
    -> T_Level_18 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> T_RawMonad_24
MAlonzo.Code.Effect.Monad.du_mkRawMonad_178
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v0 AgdaAny
v1 ->
            ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44))
      AgdaAny
forall a. a
erased
-- Relation.Nullary.Negation.¬¬-push
d_'172''172''45'push_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (((AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'172''172''45'push_70 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (((AgdaAny -> AgdaAny) -> T_Irrelevant_20) -> T_Irrelevant_20)
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
d_'172''172''45'push_70 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (((AgdaAny -> AgdaAny) -> T_Irrelevant_20) -> T_Irrelevant_20)
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.call/cc
d_call'47'cc_80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  ((AgdaAny -> AgdaAny) ->
   (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_call'47'cc_80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> AgdaAny)
    -> (AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
d_call'47'cc_80 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> ((AgdaAny -> AgdaAny)
    -> (AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.independence-of-premise
d_independence'45'of'45'premise_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_independence'45'of'45'premise_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> T_Σ_14)
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_Irrelevant_20
d_independence'45'of'45'premise_88 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> T_Σ_14)
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation._.helper
d_helper_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_helper_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> (AgdaAny -> T_Σ_14)
-> T_Dec_20
-> T_Σ_14
d_helper_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny
v6 AgdaAny -> T_Σ_14
v7 T_Dec_20
v8
  = AgdaAny -> (AgdaAny -> T_Σ_14) -> T_Dec_20 -> T_Σ_14
du_helper_106 AgdaAny
v6 AgdaAny -> T_Σ_14
v7 T_Dec_20
v8
du_helper_106 ::
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_helper_106 :: AgdaAny -> (AgdaAny -> T_Σ_14) -> T_Dec_20 -> T_Σ_14
du_helper_106 AgdaAny
v0 AgdaAny -> T_Σ_14
v1 T_Dec_20
v2
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
             then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v4 of
                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v5
                      -> ((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8322'_150 (\ AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 -> AgdaAny
v7)
                           ((AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Σ_14
v1 AgdaAny
v5)
                    T_Reflects_16
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v4)
                    ((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
v0)
                       ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                          (\ AgdaAny
v5 ->
                             ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                               AgdaAny
forall a. a
erased)))
      T_Dec_20
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Negation.independence-of-premise-⊎
d_independence'45'of'45'premise'45''8846'_112 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_independence'45'of'45'premise'45''8846'_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T__'8846'__30)
-> (T__'8846'__30 -> T_Irrelevant_20)
-> T_Irrelevant_20
d_independence'45'of'45'premise'45''8846'_112 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T__'8846'__30)
-> (T__'8846'__30 -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation._.helper
d_helper_126 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_helper_126 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T__'8846'__30)
-> T_Dec_20
-> T__'8846'__30
d_helper_126 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> T__'8846'__30
v6 T_Dec_20
v7 = (AgdaAny -> T__'8846'__30) -> T_Dec_20 -> T__'8846'__30
du_helper_126 AgdaAny -> T__'8846'__30
v6 T_Dec_20
v7
du_helper_126 ::
  (AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_helper_126 :: (AgdaAny -> T__'8846'__30) -> T_Dec_20 -> T__'8846'__30
du_helper_126 AgdaAny -> T__'8846'__30
v0 T_Dec_20
v1
  = case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v1 of
      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v2 T_Reflects_16
v3
        -> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
             then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v3 of
                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
v4
                      -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T__'8846'__30
forall a b. a -> b
coe
                           (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map_84 (\ AgdaAny
v5 AgdaAny
v6 -> AgdaAny
v5)
                           (\ AgdaAny
v5 AgdaAny
v6 -> AgdaAny
v5) ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
v0 AgdaAny
v4)
                    T_Reflects_16
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
             else (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
v3)
                    ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                       ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                          (\ AgdaAny
v4 ->
                             ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                               AgdaAny
forall a. a
erased)))
      T_Dec_20
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError