{-# 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.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Sum.Base

-- Relation.Nullary.Negation.Core.¬_
d_'172'__24 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_'172'__24 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_'172'__24 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Negation.Core.DoubleNegation
d_DoubleNegation_28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_DoubleNegation_28 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_DoubleNegation_28 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Negation.Core.Stable
d_Stable_32 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_Stable_32 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_Stable_32 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Relation.Nullary.Negation.Core._¬-⊎_
d__'172''45''8846'__36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d__'172''45''8846'__36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T__'8846'__30
-> T_Irrelevant_20
d__'172''45''8846'__36 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> T__'8846'__30
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.Core.contradiction-irr
d_contradiction'45'irr_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
d_contradiction'45'irr_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
d_contradiction'45'irr_38 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny -> T_Irrelevant_20
v5
  = AgdaAny
du_contradiction'45'irr_38
du_contradiction'45'irr_38 :: AgdaAny
du_contradiction'45'irr_38 :: AgdaAny
du_contradiction'45'irr_38
  = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.du_'8869''45'elim'45'irr_20
-- Relation.Nullary.Negation.Core.contradiction
d_contradiction_44 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
d_contradiction_44 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
d_contradiction_44 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny
v4 = (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_contradiction_44
du_contradiction_44 ::
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
du_contradiction_44 :: (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_contradiction_44 AgdaAny -> T_Irrelevant_20
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
du_contradiction'45'irr_38
-- Relation.Nullary.Negation.Core.contradiction₂
d_contradiction'8322'_48 ::
  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.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny
d_contradiction'8322'_48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T__'8846'__30
-> (AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
d_contradiction'8322'_48 ~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_Irrelevant_20
v7 ~AgdaAny -> T_Irrelevant_20
v8
  = T__'8846'__30 -> AgdaAny
du_contradiction'8322'_48 T__'8846'__30
v6
du_contradiction'8322'_48 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_contradiction'8322'_48 :: T__'8846'__30 -> AgdaAny
du_contradiction'8322'_48 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 -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Irrelevant_20) -> AgdaAny
du_contradiction_44 AgdaAny
forall a. a
erased)
-- Relation.Nullary.Negation.Core.contraposition
d_contraposition_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_contraposition_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_contraposition_62 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.Core.stable
d_stable_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  ((((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_stable_70 :: T_Level_18
-> T_Level_18
-> ((((AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20) -> AgdaAny)
    -> T_Irrelevant_20)
-> T_Irrelevant_20
d_stable_70 = T_Level_18
-> T_Level_18
-> ((((AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20) -> AgdaAny)
    -> T_Irrelevant_20)
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.Core.negated-stable
d_negated'45'stable_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (((AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_negated'45'stable_74 :: T_Level_18
-> T_Level_18
-> (((AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20)
    -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
d_negated'45'stable_74 = T_Level_18
-> T_Level_18
-> (((AgdaAny -> T_Irrelevant_20) -> T_Irrelevant_20)
    -> T_Irrelevant_20)
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Nullary.Negation.Core.¬¬-map
d_'172''172''45'map_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_'172''172''45'map_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_'172''172''45'map_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