| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.List.Relation.Binary.Lex
Documentation
d__'8779'__28 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d__'60'__30 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → [AgdaAny] → [AgdaAny] → () Source #
d_'172''8804''45'this_40 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → (AgdaAny → T_Irrelevant_20) → (AgdaAny → T_Irrelevant_20) → T_Lex_32 → T_Irrelevant_20 Source #
d_'172''8804''45'next_64 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → (AgdaAny → T_Irrelevant_20) → (T_Lex_32 → T_Irrelevant_20) → T_Lex_32 → T_Irrelevant_20 Source #
d_antisymmetric_78 ∷ 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_antisymmetric_78 ∷ [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
d_as_90 ∷ 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] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Pointwise_48 Source #
d_toSum_124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Lex_32 → T__'8846'__30 Source #
d_transitive_132 ∷ 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_transitive_132 ∷ 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_trans_144 ∷ 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] → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Lex_32 → T_Lex_32 → T_Lex_32 Source #
du_trans_144 ∷ 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_respects'8322'_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_Σ_14 → T_Σ_14 Source #
d_resp'185'_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 → T_Lex_32 Source #
du_resp'185'_200 ∷ T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 → T_Lex_32 Source #
d_resp'178'_218 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 → T_Lex_32 Source #
du_resp'178'_218 ∷ T_IsEquivalence_26 → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → [AgdaAny] → [AgdaAny] → [AgdaAny] → T_Pointwise_48 → T_Lex_32 → T_Lex_32 Source #
d_'91''93''60''91''93''45''8660'_234 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Equivalence_1714 Source #
d_'46'extendedlambda0_236 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Lex_32 → AgdaAny Source #
d_'8759''60''8759''45''8660'_248 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → [AgdaAny] → [AgdaAny] → T_Equivalence_1714 Source #
d_decidable_260 ∷ T_Level_18 → T_Level_18 → T_Level_18 → () → () → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Dec_20 → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → [AgdaAny] → [AgdaAny] → T_Dec_20 Source #