| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.On
Documentation
d_implies_38 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_implies_38 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_reflexive_44 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_irreflexive_52 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #
d_symmetric_58 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_symmetric_58 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_transitive_64 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_transitive_64 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_antisymmetric_72 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisymmetric_72 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_asymmetric_78 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #
d_respects_86 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_respects_86 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_respects'8322'_94 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_decidable_102 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_decidable_102 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_total_112 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_total_112 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_trichotomous_124 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → AgdaAny → AgdaAny → T_Tri_158 Source #
du_trichotomous_124 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_158) → AgdaAny → AgdaAny → T_Tri_158 Source #
d_accessible_136 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → T_Acc_42 → T_Acc_42 Source #
d_wellFounded_144 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #
d_isEquivalence_164 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
d_isDecEquivalence_184 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
du_isDecEquivalence_184 ∷ (AgdaAny → AgdaAny) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
d_isPreorder_226 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 Source #
d_isPartialOrder_268 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_174 → T_IsPartialOrder_174 Source #
d_isDecPartialOrder_314 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_224 → T_IsDecPartialOrder_224 Source #
du_isDecPartialOrder_314 ∷ (AgdaAny → AgdaAny) → T_IsDecPartialOrder_224 → T_IsDecPartialOrder_224 Source #
d_isStrictPartialOrder_372 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_290 → T_IsStrictPartialOrder_290 Source #
du_isStrictPartialOrder_372 ∷ (AgdaAny → AgdaAny) → T_IsStrictPartialOrder_290 → T_IsStrictPartialOrder_290 Source #
d_isTotalOrder_408 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_404 → T_IsTotalOrder_404 Source #
d_isDecTotalOrder_460 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_460 → T_IsDecTotalOrder_460 Source #
du_isDecTotalOrder_460 ∷ (AgdaAny → AgdaAny) → T_IsDecTotalOrder_460 → T_IsDecTotalOrder_460 Source #
d_isStrictTotalOrder_526 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsStrictTotalOrder_534 Source #
du_isStrictTotalOrder_526 ∷ (AgdaAny → AgdaAny) → T_IsStrictTotalOrder_534 → T_IsStrictTotalOrder_534 Source #
d_preorder_582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_Preorder_132 → (AgdaAny → AgdaAny) → T_Preorder_132 Source #
du_preorder_582 ∷ T_Preorder_132 → (AgdaAny → AgdaAny) → T_Preorder_132 Source #
d_setoid_590 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_Setoid_44 → (AgdaAny → AgdaAny) → T_Setoid_44 Source #
du_setoid_590 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → T_Setoid_44 Source #
d_decSetoid_598 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecSetoid_84 → (AgdaAny → AgdaAny) → T_DecSetoid_84 Source #
d_poset_606 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_Poset_314 → (AgdaAny → AgdaAny) → T_Poset_314 Source #
du_poset_606 ∷ T_Poset_314 → (AgdaAny → AgdaAny) → T_Poset_314 Source #
d_decPoset_614 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecPoset_406 → (AgdaAny → AgdaAny) → T_DecPoset_406 Source #
du_decPoset_614 ∷ T_DecPoset_406 → (AgdaAny → AgdaAny) → T_DecPoset_406 Source #
d_strictPartialOrder_622 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_StrictPartialOrder_556 → (AgdaAny → AgdaAny) → T_StrictPartialOrder_556 Source #
du_strictPartialOrder_622 ∷ T_StrictPartialOrder_556 → (AgdaAny → AgdaAny) → T_StrictPartialOrder_556 Source #
d_totalOrder_630 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_TotalOrder_764 → (AgdaAny → AgdaAny) → T_TotalOrder_764 Source #
d_decTotalOrder_638 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecTotalOrder_866 → (AgdaAny → AgdaAny) → T_DecTotalOrder_866 Source #
d_strictTotalOrder_646 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_StrictTotalOrder_1036 → (AgdaAny → AgdaAny) → T_StrictTotalOrder_1036 Source #