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