| 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_28 → 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_28 → 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_28 → 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_370 → T_IsStrictPartialOrder_370 Source #
du_'60''45'isStrictPartialOrder_278 ∷ T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_'60''45'isStrictTotalOrder_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsStrictTotalOrder_624 Source #
d_'60''45'strictPartialOrder_374 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_StrictPartialOrder_760 Source #
d_'60''45'strictTotalOrder_450 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_StrictTotalOrder_1280 Source #
d_'8804''45'reflexive_560 ∷ 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_560 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 Source #
d__'8779'__582 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d__'8804'__584 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d_'8804''45'antisymmetric_586 ∷ 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_586 ∷ (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_588 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → 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_588 ∷ T_IsEquivalence_28 → 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_590 ∷ 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_590 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_158) → [AgdaAny] → [AgdaAny] → T__'8846'__30 Source #
d_'8804''45'decidable_694 ∷ 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_694 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #
d_'8804''45'respects'8322'_696 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_Σ_14 → T_Σ_14 Source #
d_'8804''45'isPreorder_698 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_IsPreorder_76 Source #
du_'8804''45'isPreorder_698 ∷ T_IsEquivalence_28 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_IsPreorder_76 Source #
d_'8804''45'isPartialOrder_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsPartialOrder_248 Source #
d_'8804''45'isDecPartialOrder_742 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsDecPartialOrder_300 Source #
d_'8804''45'isTotalOrder_796 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsTotalOrder_488 Source #
d_'8804''45'isDecTotalOrder_850 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_624 → T_IsDecTotalOrder_546 Source #
d_'8804''45'preorder_910 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_Preorder_142 Source #
d_'8804''45'partialOrder_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_Poset_492 Source #
d_'8804''45'decPoset_1070 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_1280 → T_DecPoset_596 Source #