| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Properties.Poset
Documentation
d__'8819'__24 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #
d__'8934'__26 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #
d__'8777'__64 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #
d_converse'45'isPreorder_134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_IsPreorder_70 Source #
d_converse'45'preorder_136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_Preorder_132 Source #
d_'8805''45'isPartialOrder_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_IsPartialOrder_174 Source #
d_antisym_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisym_148 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_refl_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny Source #
du_refl_150 ∷ T_Poset_314 → AgdaAny → AgdaAny Source #
d_reflexive_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_reflexive_152 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_154 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8816''45'resp'737''45''8776'_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #
d_'8816''45'resp'691''45''8776'_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #
d__'60'__168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #
d_'60''45'isStrictPartialOrder_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_IsStrictPartialOrder_290 Source #
d_'60''45'strictPartialOrder_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_StrictPartialOrder_556 Source #
d__'8814'__176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → () Source #
d_asym_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_irrefl_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'60''45'resp'691''45''8776'_184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_'60''45'resp'691''45''8776'_184 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_'60''45'resp'737''45''8776'_186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_'60''45'resp'737''45''8776'_186 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_trans_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_trans_188 ∷ T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'60''8658''8777'_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Irrelevant_20 Source #
d_'8804''8743''8777''8658''60'_200 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Σ_14 Source #
d_'60''8658''8817'_206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Irrelevant_20 Source #
d_'8804''8658''8815'_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'8804''45'dec'8658''8776''45'dec_214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_'8804''45'dec'8658''8776''45'dec_214 ∷ T_Poset_314 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_'8804''45'dec'8658'isDecPartialOrder_258 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_224 Source #
du_'8804''45'dec'8658'isDecPartialOrder_258 ∷ T_Poset_314 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_224 Source #
d_mono'8658'cong_264 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'8658'cong_264 ∷ T_Poset_314 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_antimono'8658'cong_268 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #