| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Construct.Flip.EqAndOrd
Documentation
d_refl_44 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #
d_sym_48 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_sym_48 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_trans_52 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_trans_52 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_asym_56 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #
d_total_60 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 #
du_total_60 :: (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> T__'8846'__30 #
d_resp_72 :: 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 -> AgdaAny #
du_resp_72 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_max_82 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #
d_min_88 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny #
d_reflexive_106 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_reflexive_106 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_irrefl_112 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20 #
d_antisym_122 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
du_antisym_122 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny #
d_compare_126 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> T_Tri_158 #
d_resp'8322'_188 :: T_Level_18 -> () -> T_Level_18 -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14 #
du_resp'8322'_188 :: T_Σ_14 -> T_Σ_14 #
d_dec_206 :: T_Level_18 -> () -> T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> (AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> T_Dec_20 #
d_isEquivalence_210 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsEquivalence_26 -> T_IsEquivalence_26 #
d_isDecEquivalence_232 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecEquivalence_44 -> T_IsDecEquivalence_44 #
d_isPreorder_258 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPreorder_70 -> T_IsPreorder_70 #
d_isTotalPreorder_304 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalPreorder_124 -> T_IsTotalPreorder_124 #
d_isPartialOrder_350 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsPartialOrder_174 -> T_IsPartialOrder_174 #
d_isTotalOrder_398 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsTotalOrder_404 -> T_IsTotalOrder_404 #
d_isDecTotalOrder_450 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsDecTotalOrder_460 -> T_IsDecTotalOrder_460 #
d_isStrictPartialOrder_516 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290 #
d_isStrictTotalOrder_554 :: T_Level_18 -> () -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534 #
d_setoid_610 :: T_Level_18 -> T_Level_18 -> T_Setoid_44 -> T_Setoid_44 #
du_setoid_610 :: T_Setoid_44 -> T_Setoid_44 #
d_decSetoid_640 :: T_Level_18 -> T_Level_18 -> T_DecSetoid_84 -> T_DecSetoid_84 #
d_preorder_676 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132 #
d_totalPreorder_746 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalPreorder_222 -> T_TotalPreorder_222 #
d_poset_822 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_Poset_314 -> T_Poset_314 #
du_poset_822 :: T_Poset_314 -> T_Poset_314 #
d_totalOrder_898 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_TotalOrder_764 -> T_TotalOrder_764 #
d_decTotalOrder_984 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_DecTotalOrder_866 -> T_DecTotalOrder_866 #
d_strictPartialOrder_1088 :: T_Level_18 -> T_Level_18 -> T_Level_18 -> T_StrictPartialOrder_556 -> T_StrictPartialOrder_556 #