| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Binary.Lex.Strict
Documentation
d__'8779'__32 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d__'60'__34 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d_xs'8814''91''93'_38 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → T_Lex_32 → T_Irrelevant_20 Source #
d_'172''91''93''60''91''93'_40 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Lex_32 → T_Irrelevant_20 Source #
d_'60''45'irreflexive_42 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 → T_Irrelevant_20 Source #
d_'60''45'asymmetric_60 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Irrelevant_20 Source #
d_irrefl_72 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20 Source #
d_asym_74 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Irrelevant_20 Source #
d_'60''45'antisymmetric_102 ∷ 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) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
du_'60''45'antisymmetric_102 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
d_'60''45'transitive_104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Lex_32 Source #
du_'60''45'transitive_104 ∷ T_IsEquivalence_26 → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Lex_32 Source #
d_'60''45'compare_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_158) → [AgdaAny] → [AgdaAny] → T_Tri_158 Source #
du_'60''45'compare_106 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_158) → [AgdaAny] → [AgdaAny] → T_Tri_158 Source #
d_'60''45'decidable_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #
du_'60''45'decidable_274 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #
d_'60''45'respects'8322'_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_Σ_14 → T_Σ_14 Source #
d_'60''45'isStrictPartialOrder_278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_290 → T_IsStrictPartialOrder_290 Source #
du_'60''45'isStrictPartialOrder_278 ∷ T_IsStrictPartialOrder_290 → T_IsStrictPartialOrder_290 Source #
d_'60''45'isStrictTotalOrder_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsStrictTotalOrder_534 Source #
d_'60''45'strictPartialOrder_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → T_StrictPartialOrder_556 Source #
d_'60''45'strictTotalOrder_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_StrictTotalOrder_1036 Source #
d_'8804''45'reflexive_544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 Source #
du_'8804''45'reflexive_544 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 Source #
d__'8779'__566 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d__'8804'__568 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d_'8804''45'antisymmetric_570 ∷ 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) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
du_'8804''45'antisymmetric_570 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
d_'8804''45'transitive_572 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Lex_32 Source #
du_'8804''45'transitive_572 ∷ T_IsEquivalence_26 → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Lex_32 Source #
d_'8804''45'total_574 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_158) → [AgdaAny] → [AgdaAny] → T__'8846'__30 Source #
du_'8804''45'total_574 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_158) → [AgdaAny] → [AgdaAny] → T__'8846'__30 Source #
d_'8804''45'decidable_678 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #
du_'8804''45'decidable_678 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #
d_'8804''45'respects'8322'_680 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_Σ_14 → T_Σ_14 Source #
d_'8804''45'isPreorder_682 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_IsPreorder_70 Source #
du_'8804''45'isPreorder_682 ∷ T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_IsPreorder_70 Source #
d_'8804''45'isPartialOrder_690 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_290 → T_IsPartialOrder_174 Source #
d_'8804''45'isDecPartialOrder_726 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsDecPartialOrder_224 Source #
d_'8804''45'isTotalOrder_780 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsTotalOrder_404 Source #
d_'8804''45'isDecTotalOrder_834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_534 → T_IsDecTotalOrder_460 Source #
d_'8804''45'preorder_894 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Preorder_132 Source #
d_'8804''45'partialOrder_970 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_556 → T_Poset_314 Source #
d_'8804''45'decPoset_1038 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1036 → T_DecPoset_406 Source #