| Safe Haskell | None |
|---|
MAlonzo.Code.Relation.Binary.Construct.On
Documentation
d_implies_38 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_implies_38 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_reflexive_44 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny Source #
d_irreflexive_52 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #
d_symmetric_58 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_symmetric_58 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_transitive_64 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_transitive_64 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_antisymmetric_72 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_antisymmetric_72 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_asymmetric_78 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4 Source #
d_respects_86 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
du_respects_86 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny Source #
d_respects'8322'_94 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 Source #
d_decidable_102 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32 Source #
du_decidable_102 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> T_Dec_32 Source #
d_total_112 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #
du_total_112 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 Source #
d_trichotomous_124 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Tri_136 Source #
du_trichotomous_124 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Tri_136 Source #
d_accessible_136 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42 Source #
d_wellFounded_146 :: T_Level_14 -> () -> T_Level_14 -> () -> (AgdaAny -> AgdaAny) -> T_Level_14 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 Source #
d_isEquivalence_166 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsEquivalence_26 Source #
du_isEquivalence_166 :: (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26 Source #
d_isDecEquivalence_186 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 Source #
du_isDecEquivalence_186 :: (AgdaAny -> AgdaAny) -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 Source #
d_isPreorder_228 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 Source #
du_isPreorder_228 :: (AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70 Source #
d_isPartialOrder_264 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_162 -> T_IsPartialOrder_162 Source #
du_isPartialOrder_264 :: (AgdaAny -> AgdaAny) -> T_IsPartialOrder_162 -> T_IsPartialOrder_162 Source #
d_isDecPartialOrder_304 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206 Source #
du_isDecPartialOrder_304 :: (AgdaAny -> AgdaAny) -> T_IsDecPartialOrder_206 -> T_IsDecPartialOrder_206 Source #
d_isStrictPartialOrder_356 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266 Source #
du_isStrictPartialOrder_356 :: (AgdaAny -> AgdaAny) -> T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266 Source #
d_isTotalOrder_392 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_380 -> T_IsTotalOrder_380 Source #
du_isTotalOrder_392 :: (AgdaAny -> AgdaAny) -> T_IsTotalOrder_380 -> T_IsTotalOrder_380 Source #
d_isDecTotalOrder_438 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_430 -> T_IsDecTotalOrder_430 Source #
du_isDecTotalOrder_438 :: (AgdaAny -> AgdaAny) -> T_IsDecTotalOrder_430 -> T_IsDecTotalOrder_430 Source #
d_isStrictTotalOrder_498 :: T_Level_14 -> () -> T_Level_14 -> () -> T_Level_14 -> T_Level_14 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_498 -> T_IsStrictTotalOrder_498 Source #
du_isStrictTotalOrder_498 :: (AgdaAny -> AgdaAny) -> T_IsStrictTotalOrder_498 -> T_IsStrictTotalOrder_498 Source #
d_preorder_552 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_Preorder_132 -> (AgdaAny -> AgdaAny) -> T_Preorder_132 Source #
du_preorder_552 :: T_Preorder_132 -> (AgdaAny -> AgdaAny) -> T_Preorder_132 Source #
d_setoid_560 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Setoid_44 Source #
du_setoid_560 :: T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Setoid_44 Source #
d_decSetoid_568 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_DecSetoid_84 -> (AgdaAny -> AgdaAny) -> T_DecSetoid_84 Source #
du_decSetoid_568 :: T_DecSetoid_84 -> (AgdaAny -> AgdaAny) -> T_DecSetoid_84 Source #
d_poset_576 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_Poset_282 -> (AgdaAny -> AgdaAny) -> T_Poset_282 Source #
du_poset_576 :: T_Poset_282 -> (AgdaAny -> AgdaAny) -> T_Poset_282 Source #
d_decPoset_584 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_DecPoset_360 -> (AgdaAny -> AgdaAny) -> T_DecPoset_360 Source #
du_decPoset_584 :: T_DecPoset_360 -> (AgdaAny -> AgdaAny) -> T_DecPoset_360 Source #
d_strictPartialOrder_592 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_StrictPartialOrder_472 -> (AgdaAny -> AgdaAny) -> T_StrictPartialOrder_472 Source #
du_strictPartialOrder_592 :: T_StrictPartialOrder_472 -> (AgdaAny -> AgdaAny) -> T_StrictPartialOrder_472 Source #
d_totalOrder_600 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_TotalOrder_648 -> (AgdaAny -> AgdaAny) -> T_TotalOrder_648 Source #
du_totalOrder_600 :: T_TotalOrder_648 -> (AgdaAny -> AgdaAny) -> T_TotalOrder_648 Source #
d_decTotalOrder_608 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_DecTotalOrder_736 -> (AgdaAny -> AgdaAny) -> T_DecTotalOrder_736 Source #
du_decTotalOrder_608 :: T_DecTotalOrder_736 -> (AgdaAny -> AgdaAny) -> T_DecTotalOrder_736 Source #
d_strictTotalOrder_616 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> () -> T_StrictTotalOrder_860 -> (AgdaAny -> AgdaAny) -> T_StrictTotalOrder_860 Source #