| 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_156 ∷ p → p → p → p → p → p → () Source #
d_IsMagma_196 ∷ p → p → p → p → p → p → () Source #
d_IsSemigroup_224 ∷ p → p → p → p → p → p → () Source #
d_idem_338 ∷ T_IsBand_508 → AgdaAny → AgdaAny Source #
d_'8729''45'cong_1510 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_2350 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_IsSemilattice_2682 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d__'8804'__3088 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → () Source #
d_reflexive_3094 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_reflexive_3094 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_refl_3172 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_refl_3172 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_antisym_3180 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisym_3180 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_total_3250 ∷ 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_3250 ∷ (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_3266 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_3266 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_resp'691'_3350 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_resp'691'_3350 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_resp'737'_3430 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_resp'737'_3430 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_resp'8322'_3510 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → T_Σ_14 Source #
du_resp'8322'_3510 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsMagma_176 → T_Σ_14 Source #
d_dec_3514 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_dec_3514 ∷ (AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_x'8729'y'8804'x_3606 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8729'y'8804'x_3606 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8729'y'8804'y_3616 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8729'y'8804'y_3616 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8729''45'pres'691''45''8804'_3628 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8729''45'pres'691''45''8804'_3628 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_infimum_3640 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T_Σ_14 Source #
du_infimum_3640 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → AgdaAny → AgdaAny → T_Σ_14 Source #
d_isPreorder_3646 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_IsPreorder_70 Source #
du_isPreorder_3646 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_IsPreorder_70 Source #
d_isPartialOrder_3680 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsPartialOrder_174 Source #
du_isPartialOrder_3680 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_IsPartialOrder_174 Source #
d_isDecPartialOrder_3722 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_224 Source #
du_isDecPartialOrder_3722 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_224 Source #
d_isTotalOrder_3728 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → T_IsTotalOrder_404 Source #
du_isTotalOrder_3728 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → T_IsTotalOrder_404 Source #
d_isDecTotalOrder_3772 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecTotalOrder_460 Source #
du_isDecTotalOrder_3772 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecTotalOrder_460 Source #
d_preorder_3780 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_Preorder_132 Source #
du_preorder_3780 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsBand_508 → T_Preorder_132 Source #
d_poset_3784 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_Poset_314 Source #
du_poset_3784 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → T_Poset_314 Source #
d_decPoset_3788 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T_Dec_20) → T_DecPoset_406 Source #
du_decPoset_3788 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T_Dec_20) → T_DecPoset_406 Source #
d_totalOrder_3794 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → T_TotalOrder_764 Source #
du_totalOrder_3794 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → T_TotalOrder_764 Source #
d_decTotalOrder_3800 ∷ T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_DecTotalOrder_866 Source #
du_decTotalOrder_3800 ∷ (AgdaAny → AgdaAny → AgdaAny) → T_IsCommutativeBand_590 → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T_Dec_20) → T_DecTotalOrder_866 Source #