| 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_'8869'_4) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 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_'8869'_4) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 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_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
du_decidable_102 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 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_136) → AgdaAny → AgdaAny → T_Tri_136 Source #
du_trichotomous_124 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_136) → AgdaAny → AgdaAny → T_Tri_136 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_146 ∷ T_Level_18 → () → T_Level_18 → () → (AgdaAny → AgdaAny) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → AgdaAny → T_Acc_42 Source #
d_isEquivalence_166 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
d_isDecEquivalence_186 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
du_isDecEquivalence_186 ∷ (AgdaAny → AgdaAny) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
d_isPreorder_228 ∷ 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_264 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
d_isDecPartialOrder_304 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecPartialOrder_206 → T_IsDecPartialOrder_206 Source #
du_isDecPartialOrder_304 ∷ (AgdaAny → AgdaAny) → T_IsDecPartialOrder_206 → T_IsDecPartialOrder_206 Source #
d_isStrictPartialOrder_356 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
du_isStrictPartialOrder_356 ∷ (AgdaAny → AgdaAny) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_isTotalOrder_394 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → T_IsTotalOrder_384 Source #
d_isDecTotalOrder_440 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsDecTotalOrder_434 Source #
du_isDecTotalOrder_440 ∷ (AgdaAny → AgdaAny) → T_IsDecTotalOrder_434 → T_IsDecTotalOrder_434 Source #
d_isStrictTotalOrder_500 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
du_isStrictTotalOrder_500 ∷ (AgdaAny → AgdaAny) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
d_preorder_554 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_Preorder_132 → (AgdaAny → AgdaAny) → T_Preorder_132 Source #
du_preorder_554 ∷ T_Preorder_132 → (AgdaAny → AgdaAny) → T_Preorder_132 Source #
d_setoid_562 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_Setoid_44 → (AgdaAny → AgdaAny) → T_Setoid_44 Source #
du_setoid_562 ∷ T_Setoid_44 → (AgdaAny → AgdaAny) → T_Setoid_44 Source #
d_decSetoid_570 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecSetoid_84 → (AgdaAny → AgdaAny) → T_DecSetoid_84 Source #
d_poset_578 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_Poset_282 → (AgdaAny → AgdaAny) → T_Poset_282 Source #
du_poset_578 ∷ T_Poset_282 → (AgdaAny → AgdaAny) → T_Poset_282 Source #
d_decPoset_586 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecPoset_360 → (AgdaAny → AgdaAny) → T_DecPoset_360 Source #
du_decPoset_586 ∷ T_DecPoset_360 → (AgdaAny → AgdaAny) → T_DecPoset_360 Source #
d_strictPartialOrder_594 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_StrictPartialOrder_472 → (AgdaAny → AgdaAny) → T_StrictPartialOrder_472 Source #
du_strictPartialOrder_594 ∷ T_StrictPartialOrder_472 → (AgdaAny → AgdaAny) → T_StrictPartialOrder_472 Source #
d_totalOrder_602 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_TotalOrder_652 → (AgdaAny → AgdaAny) → T_TotalOrder_652 Source #
d_decTotalOrder_610 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_DecTotalOrder_740 → (AgdaAny → AgdaAny) → T_DecTotalOrder_740 Source #
d_strictTotalOrder_618 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → () → T_StrictTotalOrder_864 → (AgdaAny → AgdaAny) → T_StrictTotalOrder_864 Source #