| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Nullary.Negation
Documentation
d_'8707''10230''172''8704''172'_32 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Σ_14 → (AgdaAny → AgdaAny → T_Irrelevant_20) → T_Irrelevant_20 Source #
d_'8704''10230''172''8707''172'_38 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Irrelevant_20 Source #
d_'172''8707''10230''8704''172'_50 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (T_Σ_14 → T_Irrelevant_20) → AgdaAny → AgdaAny → T_Irrelevant_20 Source #
d_'8704''172''10230''172''8707'_56 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (AgdaAny → AgdaAny → T_Irrelevant_20) → T_Σ_14 → T_Irrelevant_20 Source #
d_'8707''172''10230''172''8704'_62 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → T_Σ_14 → (AgdaAny → AgdaAny) → T_Irrelevant_20 Source #
d_'172''172''45'push_70 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → (((AgdaAny → AgdaAny) → T_Irrelevant_20) → T_Irrelevant_20) → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Irrelevant_20 Source #
d_call'47'cc_80 ∷ T_Level_18 → () → T_Level_18 → () → ((AgdaAny → AgdaAny) → (AgdaAny → T_Irrelevant_20) → T_Irrelevant_20) → (AgdaAny → T_Irrelevant_20) → T_Irrelevant_20 Source #
d_independence'45'of'45'premise_88 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → (AgdaAny → T_Σ_14) → (T_Σ_14 → T_Irrelevant_20) → T_Irrelevant_20 Source #
d_helper_106 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → ()) → AgdaAny → (AgdaAny → T_Σ_14) → T_Dec_20 → T_Σ_14 Source #
d_independence'45'of'45'premise'45''8846'_112 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T__'8846'__30) → (T__'8846'__30 → T_Irrelevant_20) → T_Irrelevant_20 Source #
d_helper_126 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → (AgdaAny → T__'8846'__30) → T_Dec_20 → T__'8846'__30 Source #
du_helper_126 ∷ (AgdaAny → T__'8846'__30) → T_Dec_20 → T__'8846'__30 Source #