{-# 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
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
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
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
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
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
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
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)
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
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
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
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