| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Relation.Binary.Properties.Poset
Documentation
d__'8777'__22 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #
d__'8764''7506'__26 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #
d__'8769'__28 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #
d_converse'45'isPreorder_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_IsPreorder_76 Source #
d_converse'45'preorder_144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Preorder_142 Source #
d_'8805''45'isPartialOrder_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_IsPartialOrder_248 Source #
d_antisym_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_antisym_156 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_refl_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny Source #
du_refl_158 ∷ T_Poset_492 → AgdaAny → AgdaAny Source #
d_reflexive_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_reflexive_160 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_trans_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_trans_162 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8816''45'resp'737''45''8776'_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #
d_'8816''45'resp'691''45''8776'_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → AgdaAny → T_Irrelevant_20 Source #
d__'60'__176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #
d_'60''45'isStrictPartialOrder_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_IsStrictPartialOrder_370 Source #
d_'60''45'strictPartialOrder_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_StrictPartialOrder_760 Source #
d__'8769'__184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → () Source #
d_asym_186 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_irrefl_188 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'60''45'resp'691''45''8776'_192 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_'60''45'resp'691''45''8776'_192 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_'60''45'resp'737''45''8776'_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
du_'60''45'resp'737''45''8776'_194 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 Source #
d_trans_196 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_trans_196 ∷ T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'60''8658''8777'_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Irrelevant_20 Source #
d_'8804''8743''8777''8658''60'_208 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → (AgdaAny → T_Irrelevant_20) → T_Σ_14 Source #
d_'60''8658''8817'_214 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → T_Σ_14 → AgdaAny → T_Irrelevant_20 Source #
d_'8804''8658''8815'_220 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → AgdaAny → AgdaAny → AgdaAny → T_Σ_14 → T_Irrelevant_20 Source #
d_'8804''45'dec'8658''8776''45'dec_222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
du_'8804''45'dec'8658''8776''45'dec_222 ∷ T_Poset_492 → (AgdaAny → AgdaAny → T_Dec_20) → AgdaAny → AgdaAny → T_Dec_20 Source #
d_'8804''45'dec'8658'isDecPartialOrder_266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_300 Source #
du_'8804''45'dec'8658'isDecPartialOrder_266 ∷ T_Poset_492 → (AgdaAny → AgdaAny → T_Dec_20) → T_IsDecPartialOrder_300 Source #
d_mono'8658'cong_272 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'8658'cong_272 ∷ T_Poset_492 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_antimono'8658'cong_276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #