| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd
Documentation
d_refl_44 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_sym_48 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_sym_48 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_52 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_52 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_asym_56 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #
d_total_60 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_total_60 ∷ (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_resp_72 ∷ 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 → AgdaAny Source #
du_resp_72 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_max_82 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_min_88 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_reflexive_106 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_reflexive_106 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_irrefl_112 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #
d_antisym_122 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisym_122 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_compare_126 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_158) → AgdaAny → AgdaAny → T_Tri_158 Source #
d_resp'8322'_188 ∷ T_Level_18 → () → T_Level_18 → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_dec_206 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_isEquivalence_210 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsEquivalence_28 Source #
d_isDecEquivalence_232 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #
d_isPreorder_258 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → T_IsPreorder_76 Source #
d_isTotalPreorder_304 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_132 → T_IsTotalPreorder_132 Source #
d_isPartialOrder_350 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → T_IsPartialOrder_248 Source #
d_isTotalOrder_398 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_488 → T_IsTotalOrder_488 Source #
d_isDecTotalOrder_450 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_546 → T_IsDecTotalOrder_546 Source #
d_isStrictPartialOrder_518 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_isStrictTotalOrder_556 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
d_totalPreorder_760 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_TotalPreorder_240 Source #
d_totalOrder_928 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_986 → T_TotalOrder_986 Source #
d_decTotalOrder_1022 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_1098 → T_DecTotalOrder_1098 Source #
d_strictPartialOrder_1134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_StrictPartialOrder_760 Source #