| 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_28 → T_IsEquivalence_28 Source #
d_isDecEquivalence_184 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #
du_isDecEquivalence_184 ∷ (AgdaAny → AgdaAny) → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #
d_isPreorder_226 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → T_IsPreorder_76 Source #
d_isPartialOrder_268 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → T_IsPartialOrder_248 Source #
d_isDecPartialOrder_314 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_300 → T_IsDecPartialOrder_300 Source #
du_isDecPartialOrder_314 ∷ (AgdaAny → AgdaAny) → T_IsDecPartialOrder_300 → T_IsDecPartialOrder_300 Source #
d_isStrictPartialOrder_374 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
du_isStrictPartialOrder_374 ∷ (AgdaAny → AgdaAny) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_isTotalOrder_410 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → T_IsTotalOrder_488 Source #
d_isDecTotalOrder_462 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsDecTotalOrder_546 Source #
du_isDecTotalOrder_462 ∷ (AgdaAny → AgdaAny) → T_IsDecTotalOrder_546 → T_IsDecTotalOrder_546 Source #
d_isStrictTotalOrder_530 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
du_isStrictTotalOrder_530 ∷ (AgdaAny → AgdaAny) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
d_preorder_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_Preorder_142 → (AgdaAny → AgdaAny) → T_Preorder_142 Source #
du_preorder_586 ∷ T_Preorder_142 → (AgdaAny → AgdaAny) → T_Preorder_142 Source #
d_setoid_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_Setoid_46 → (AgdaAny → AgdaAny) → T_Setoid_46 Source #
du_setoid_594 ∷ T_Setoid_46 → (AgdaAny → AgdaAny) → T_Setoid_46 Source #
d_decSetoid_602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecSetoid_90 → (AgdaAny → AgdaAny) → T_DecSetoid_90 Source #
d_poset_610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_Poset_492 → (AgdaAny → AgdaAny) → T_Poset_492 Source #
du_poset_610 ∷ T_Poset_492 → (AgdaAny → AgdaAny) → T_Poset_492 Source #
d_decPoset_618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecPoset_596 → (AgdaAny → AgdaAny) → T_DecPoset_596 Source #
du_decPoset_618 ∷ T_DecPoset_596 → (AgdaAny → AgdaAny) → T_DecPoset_596 Source #
d_strictPartialOrder_626 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_StrictPartialOrder_760 → (AgdaAny → AgdaAny) → T_StrictPartialOrder_760 Source #
du_strictPartialOrder_626 ∷ T_StrictPartialOrder_760 → (AgdaAny → AgdaAny) → T_StrictPartialOrder_760 Source #
d_totalOrder_634 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_TotalOrder_986 → (AgdaAny → AgdaAny) → T_TotalOrder_986 Source #
d_decTotalOrder_642 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecTotalOrder_1098 → (AgdaAny → AgdaAny) → T_DecTotalOrder_1098 Source #
d_strictTotalOrder_650 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_StrictTotalOrder_1280 → (AgdaAny → AgdaAny) → T_StrictTotalOrder_1280 Source #