| 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_'172''91''93''60''91''93'_36 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Lex_32 → T_'8869'_4 Source #
d_'60''45'irreflexive_38 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 → T_'8869'_4 Source #
d_'60''45'asymmetric_56 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_'8869'_4 Source #
d_irrefl_68 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4 Source #
d_asym_70 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_'8869'_4 Source #
d_'60''45'antisymmetric_98 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
du_'60''45'antisymmetric_98 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
d_'60''45'transitive_100 ∷ 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_100 ∷ 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_102 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_136) → [AgdaAny] → [AgdaAny] → T_Tri_136 Source #
du_'60''45'compare_102 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_136) → [AgdaAny] → [AgdaAny] → T_Tri_136 Source #
d_'60''45'decidable_270 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T_Dec_32 Source #
du_'60''45'decidable_270 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T_Dec_32 Source #
d_'60''45'respects'8322'_272 ∷ 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_274 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
du_'60''45'isStrictPartialOrder_274 ∷ T_IsStrictPartialOrder_266 → T_IsStrictPartialOrder_266 Source #
d_'60''45'isStrictTotalOrder_312 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsStrictTotalOrder_502 Source #
d_'60''45'strictPartialOrder_370 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_StrictPartialOrder_472 Source #
d_'60''45'strictTotalOrder_434 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_StrictTotalOrder_864 Source #
d_'8804''45'reflexive_522 ∷ 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_522 ∷ [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 Source #
d__'8779'__544 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d__'8804'__546 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d_'8804''45'antisymmetric_548 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
du_'8804''45'antisymmetric_548 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_'8869'_4) → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
d_'8804''45'transitive_550 ∷ 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_550 ∷ 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_552 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_136) → [AgdaAny] → [AgdaAny] → T__'8846'__30 Source #
du_'8804''45'total_552 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T_Tri_136) → [AgdaAny] → [AgdaAny] → T__'8846'__30 Source #
d_'8804''45'decidable_656 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T_Dec_32 Source #
du_'8804''45'decidable_656 ∷ (AgdaAny → AgdaAny → T_Dec_32) → (AgdaAny → AgdaAny → T_Dec_32) → [AgdaAny] → [AgdaAny] → T_Dec_32 Source #
d_'8804''45'respects'8322'_658 ∷ 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_660 ∷ 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_660 ∷ T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_IsPreorder_70 Source #
d_'8804''45'isPartialOrder_668 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_266 → T_IsPartialOrder_162 Source #
d_'8804''45'isDecPartialOrder_706 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsDecPartialOrder_206 Source #
d_'8804''45'isTotalOrder_758 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsTotalOrder_384 Source #
d_'8804''45'isDecTotalOrder_810 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsStrictTotalOrder_502 → T_IsDecTotalOrder_434 Source #
d_'8804''45'preorder_868 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Preorder_132 Source #
d_'8804''45'partialOrder_930 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_472 → T_Poset_282 Source #
d_'8804''45'decPoset_994 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_StrictTotalOrder_864 → T_DecPoset_360 Source #