| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Converse
Documentation
d_refl_20 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_sym_24 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_sym_24 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_28 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_28 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_asym_32 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #
d_total_36 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_total_36 ∷ (AgdaAny → AgdaAny → T__'8846'__30) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_resp_48 ∷ 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_48 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_max_58 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_min_64 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_reflexive_84 ∷ 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_84 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_irrefl_90 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #
d_antisym_100 ∷ 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_100 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_compare_104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Tri_136) → AgdaAny → AgdaAny → T_Tri_136 Source #
d_resp'8322'_168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 Source #
d_dec_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → AgdaAny → AgdaAny → T_Dec_32 Source #
d_isEquivalence_206 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
d_isDecEquivalence_226 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
d_isPreorder_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPreorder_70 → T_IsPreorder_70 Source #
d_isTotalPreorder_302 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsTotalPreorder_118 → T_IsTotalPreorder_118 Source #
d_isPartialOrder_342 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_162 → T_IsPartialOrder_162 Source #
d_isTotalOrder_382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsTotalOrder_384 → T_IsTotalOrder_384 Source #
d_isDecTotalOrder_428 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsDecTotalOrder_434 → T_IsDecTotalOrder_434 Source #
d_isStrictPartialOrder_488 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_isStrictTotalOrder_526 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
d_totalPreorder_718 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_204 → T_TotalPreorder_204 Source #
d_totalOrder_842 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalOrder_652 → T_TotalOrder_652 Source #
d_decTotalOrder_914 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_DecTotalOrder_740 → T_DecTotalOrder_740 Source #
d_strictPartialOrder_1002 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_StrictPartialOrder_472 Source #