{-# 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.Core 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.Data.Empty
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Nullary

-- Relation.Nullary.Negation.Core.contradiction
d_contradiction_24 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) -> AgdaAny
d_contradiction_24 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
d_contradiction_24 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny -> T_'8869'_4
v5 = AgdaAny
du_contradiction_24
du_contradiction_24 :: AgdaAny
du_contradiction_24 :: AgdaAny
du_contradiction_24
  = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.du_'8869''45'elim_10
-- Relation.Nullary.Negation.Core.contradiction₂
d_contradiction'8322'_30 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) -> AgdaAny
d_contradiction'8322'_30 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T__'8846'__30
-> (AgdaAny -> T_'8869'_4)
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
d_contradiction'8322'_30 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 T__'8846'__30
v6 ~AgdaAny -> T_'8869'_4
v7 ~AgdaAny -> T_'8869'_4
v8
  = T__'8846'__30 -> AgdaAny
du_contradiction'8322'_30 T__'8846'__30
v6
du_contradiction'8322'_30 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_contradiction'8322'_30 :: T__'8846'__30 -> AgdaAny
du_contradiction'8322'_30 T__'8846'__30
v0
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe T__'8846'__30
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
du_contradiction_24)
-- Relation.Nullary.Negation.Core.contraposition
d_contraposition_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_contraposition_44 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
d_contraposition_44 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core.¬-reflects
d_'172''45'reflects_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Bool ->
  MAlonzo.Code.Relation.Nullary.T_Reflects_14 ->
  MAlonzo.Code.Relation.Nullary.T_Reflects_14
d_'172''45'reflects_56 :: T_Level_18 -> T_Level_18 -> Bool -> T_Reflects_14 -> T_Reflects_14
d_'172''45'reflects_56 ~T_Level_18
v0 ~T_Level_18
v1 ~Bool
v2 T_Reflects_14
v3 = T_Reflects_14 -> T_Reflects_14
du_'172''45'reflects_56 T_Reflects_14
v3
du_'172''45'reflects_56 ::
  MAlonzo.Code.Relation.Nullary.T_Reflects_14 ->
  MAlonzo.Code.Relation.Nullary.T_Reflects_14
du_'172''45'reflects_56 :: T_Reflects_14 -> T_Reflects_14
du_'172''45'reflects_56 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
        -> 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
MAlonzo.Code.Relation.Nullary.C_of'8319'_26
        -> (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
forall a. a
erased
      T_Reflects_14
_ -> T_Reflects_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Nullary.Negation.Core.¬?
d_'172''63'_64 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'172''63'_64 :: T_Level_18 -> T_Level_18 -> T_Dec_32 -> T_Dec_32
d_'172''63'_64 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_32
v2 = T_Dec_32 -> T_Dec_32
du_'172''63'_64 T_Dec_32
v2
du_'172''63'_64 ::
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'172''63'_64 :: T_Dec_32 -> T_Dec_32
du_'172''63'_64 T_Dec_32
v0
  = (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) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d_not_22
         ((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_Reflects_14 -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Reflects_14 -> T_Reflects_14
du_'172''45'reflects_56
         ((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)))
-- Relation.Nullary.Negation.Core._.∃⟶¬∀¬
d_'8707''10230''172''8704''172'_82 ::
  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.Empty.T_'8869'_4) ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8707''10230''172''8704''172'_82 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> T_'8869'_4)
-> T_'8869'_4
d_'8707''10230''172''8704''172'_82 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> T_'8869'_4)
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core._.∀⟶¬∃¬
d_'8704''10230''172''8707''172'_88 ::
  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.Empty.T_'8869'_4
d_'8704''10230''172''8707''172'_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_'8869'_4
d_'8704''10230''172''8707''172'_88 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core._.¬∃⟶∀¬
d_'172''8707''10230''8704''172'_100 ::
  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.Empty.T_'8869'_4) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_'172''8707''10230''8704''172'_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (T_Σ_14 -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_'172''8707''10230''8704''172'_100 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (T_Σ_14 -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core._.∀¬⟶¬∃
d_'8704''172''10230''172''8707'_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8704''172''10230''172''8707'_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_'8869'_4)
-> T_Σ_14
-> T_'8869'_4
d_'8704''172''10230''172''8707'_106 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_'8869'_4)
-> T_Σ_14
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core._.∃¬⟶¬∀
d_'8707''172''10230''172''8704'_112 ::
  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.Empty.T_'8869'_4
d_'8707''172''10230''172''8704'_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> T_'8869'_4
d_'8707''172''10230''172''8704'_112 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny)
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core.¬¬-map
d_'172''172''45'map_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  ((AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'172''172''45'map_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> ((AgdaAny -> T_'8869'_4) -> T_'8869'_4)
-> (AgdaAny -> T_'8869'_4)
-> T_'8869'_4
d_'172''172''45'map_114 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> ((AgdaAny -> T_'8869'_4) -> T_'8869'_4)
-> (AgdaAny -> T_'8869'_4)
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core.Stable
d_Stable_118 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_Stable_118 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_Stable_118 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Negation.Core.stable
d_stable_122 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  ((((AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
     MAlonzo.Code.Data.Empty.T_'8869'_4) ->
    AgdaAny) ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_stable_122 :: T_Level_18
-> T_Level_18
-> ((((AgdaAny -> T_'8869'_4) -> T_'8869'_4) -> AgdaAny)
    -> T_'8869'_4)
-> T_'8869'_4
d_stable_122 = T_Level_18
-> T_Level_18
-> ((((AgdaAny -> T_'8869'_4) -> T_'8869'_4) -> AgdaAny)
    -> T_'8869'_4)
-> T_'8869'_4
forall a. a
erased
-- Relation.Nullary.Negation.Core.negated-stable
d_negated'45'stable_128 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (((AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
    MAlonzo.Code.Data.Empty.T_'8869'_4) ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_negated'45'stable_128 :: T_Level_18
-> T_Level_18
-> (((AgdaAny -> T_'8869'_4) -> T_'8869'_4) -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
d_negated'45'stable_128 = T_Level_18
-> T_Level_18
-> (((AgdaAny -> T_'8869'_4) -> T_'8869'_4) -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
forall a. a
erased