| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.On
Documentation
d_implies_38 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_implies_38 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_reflexive_44 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #
d_irreflexive_52 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #
d_symmetric_58 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_symmetric_58 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_transitive_64 :: 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 #
du_transitive_64 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_antisymmetric_72 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_antisymmetric_72 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_asymmetric_78 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #
d_respects_86 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_respects_86 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_respects'8322'_94 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #
d_decidable_102 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20 #
du_decidable_102 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20 #
d_total_112 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 #
du_total_112 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 #
d_trichotomous_124 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> T_Tri_158 #
du_trichotomous_124 :: (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> T_Tri_158 #
d_accessible_136 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> T_Acc_42 -> T_Acc_42 #
d_wellFounded_144 :: T_Level_18 -> () -> T_Level_18 -> () -> (AgdaAny -> AgdaAny) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> T_Acc_42) -> AgdaAny -> T_Acc_42 #
d_isEquivalence_164 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsEquivalence_26 #
du_isEquivalence_164 :: (AgdaAny -> AgdaAny) -> T_IsEquivalence_26 -> T_IsEquivalence_26 #
d_isDecEquivalence_184 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 #
d_isPreorder_226 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 #
du_isPreorder_226 :: (AgdaAny -> AgdaAny) -> T_IsPreorder_70 -> T_IsPreorder_70 #
d_isPartialOrder_268 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 #
du_isPartialOrder_268 :: (AgdaAny -> AgdaAny) -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 #
d_isDecPartialOrder_314 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224 #
du_isDecPartialOrder_314 :: (AgdaAny -> AgdaAny) -> T_IsDecPartialOrder_224 -> T_IsDecPartialOrder_224 #
d_isStrictPartialOrder_372 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #
du_isStrictPartialOrder_372 :: (AgdaAny -> AgdaAny) -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #
d_isTotalOrder_408 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_IsTotalOrder_404 #
du_isTotalOrder_408 :: (AgdaAny -> AgdaAny) -> T_IsTotalOrder_404 -> T_IsTotalOrder_404 #
d_isDecTotalOrder_460 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsDecTotalOrder_460 #
d_isStrictTotalOrder_526 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534 #
du_isStrictTotalOrder_526 :: (AgdaAny -> AgdaAny) -> T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534 #
d_preorder_582 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_Preorder_132 -> (AgdaAny -> AgdaAny) -> T_Preorder_132 #
du_preorder_582 :: T_Preorder_132 -> (AgdaAny -> AgdaAny) -> T_Preorder_132 #
d_setoid_590 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Setoid_44 #
du_setoid_590 :: T_Setoid_44 -> (AgdaAny -> AgdaAny) -> T_Setoid_44 #
d_decSetoid_598 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_DecSetoid_84 -> (AgdaAny -> AgdaAny) -> T_DecSetoid_84 #
du_decSetoid_598 :: T_DecSetoid_84 -> (AgdaAny -> AgdaAny) -> T_DecSetoid_84 #
d_poset_606 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_Poset_314 -> (AgdaAny -> AgdaAny) -> T_Poset_314 #
du_poset_606 :: T_Poset_314 -> (AgdaAny -> AgdaAny) -> T_Poset_314 #
d_decPoset_614 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_DecPoset_406 -> (AgdaAny -> AgdaAny) -> T_DecPoset_406 #
du_decPoset_614 :: T_DecPoset_406 -> (AgdaAny -> AgdaAny) -> T_DecPoset_406 #
d_strictPartialOrder_622 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_StrictPartialOrder_556 -> (AgdaAny -> AgdaAny) -> T_StrictPartialOrder_556 #
du_strictPartialOrder_622 :: T_StrictPartialOrder_556 -> (AgdaAny -> AgdaAny) -> T_StrictPartialOrder_556 #
d_totalOrder_630 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> T_TotalOrder_764 #
du_totalOrder_630 :: T_TotalOrder_764 -> (AgdaAny -> AgdaAny) -> T_TotalOrder_764 #
d_decTotalOrder_638 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_DecTotalOrder_866 -> (AgdaAny -> AgdaAny) -> T_DecTotalOrder_866 #
du_decTotalOrder_638 :: T_DecTotalOrder_866 -> (AgdaAny -> AgdaAny) -> T_DecTotalOrder_866 #
d_strictTotalOrder_646 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Level_18 -> () -> T_StrictTotalOrder_1036 -> (AgdaAny -> AgdaAny) -> T_StrictTotalOrder_1036 #