| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.NaturalOrder.Left
Documentation
d_Commutative_48 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Idempotent_58 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Selective_130 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_IsBand_160 ∷ p → p → p → p → p → p → () Source #
d_IsMagma_240 ∷ p → p → p → p → p → p → () Source #
d_IsSemigroup_296 ∷ p → p → p → p → p → p → () Source #
d_idem_424 ∷ T_IsBand_526 → AgdaAny → AgdaAny Source #
d_'8729''45'cong_1606 ∷ T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_2448 ∷ T_IsSemigroup_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_IsSemilattice_2796 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__'8804'__3202 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #
d_reflexive_3208 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_reflexive_3208 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_refl_3286 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_refl_3286 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_antisym_3294 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_28 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisym_3294 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_28 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_total_3364 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_total_3364 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_trans_3380 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_3380 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_resp'691'_3464 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_resp'691'_3464 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_resp'737'_3544 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_resp'737'_3544 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_resp'8322'_3624 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → T_Σ_14 Source #
du_resp'8322'_3624 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_178 → T_Σ_14 Source #
d_dec_3628 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_dec_3628 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_x'8729'y'8804'x_3720 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8729'y'8804'x_3720 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8729'y'8804'y_3730 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8729'y'8804'y_3730 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'pres'691''45''8804'_3742 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'pres'691''45''8804'_3742 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_infimum_3754 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T_Σ_14 Source #
du_infimum_3754 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → AgdaAny → AgdaAny → T_Σ_14 Source #
d_isPreorder_3760 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → T_IsPreorder_76 Source #
du_isPreorder_3760 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → T_IsPreorder_76 Source #
d_isPartialOrder_3794 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsPartialOrder_248 Source #
du_isPartialOrder_3794 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_IsPartialOrder_248 Source #
d_isDecPartialOrder_3836 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_300 Source #
du_isDecPartialOrder_3836 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_300 Source #
d_isTotalOrder_3842 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → T_IsTotalOrder_488 Source #
du_isTotalOrder_3842 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → T_IsTotalOrder_488 Source #
d_isDecTotalOrder_3886 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecTotalOrder_546 Source #
du_isDecTotalOrder_3886 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecTotalOrder_546 Source #
d_preorder_3894 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → T_Preorder_142 Source #
du_preorder_3894 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_526 → T_Preorder_142 Source #
d_poset_3898 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_Poset_492 Source #
du_poset_3898 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → T_Poset_492 Source #
d_decPoset_3902 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T_Dec_20) → T_DecPoset_596 Source #
du_decPoset_3902 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T_Dec_20) → T_DecPoset_596 Source #
d_totalOrder_3908 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → T_TotalOrder_986 Source #
du_totalOrder_3908 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → T_TotalOrder_986 Source #
d_decTotalOrder_3914 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_DecTotalOrder_1098 Source #
du_decTotalOrder_3914 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_612 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_DecTotalOrder_1098 Source #