| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Product.Relation.Binary.Pointwise.NonDependent
Documentation
d_Pointwise_40 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → () Source #
d_'215''45'reflexive_54 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'reflexive_54 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'refl_60 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 Source #
d_'215''45'irreflexive'8321'_66 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'215''45'irreflexive'8322'_74 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'215''45'symmetric_82 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'symmetric_82 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'transitive_88 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'transitive_88 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'antisymmetric_94 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'antisymmetric_94 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'asymmetric'8321'_100 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'215''45'asymmetric'8322'_108 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Irrelevant_20 Source #
d_'215''45'respects'691'_116 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'respects'691'_116 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'respects'737'_122 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
du_'215''45'respects'737'_122 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'respects'8322'_128 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'215''45'total_130 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T__'8846'__30) → T_Σ_14 → T_Σ_14 → T__'8846'__30 Source #
du_'215''45'total_130 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → T__'8846'__30) → (AgdaAny → AgdaAny → T__'8846'__30) → T_Σ_14 → T_Σ_14 → T__'8846'__30 Source #
d_'215''45'decidable_222 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → T_Σ_14 → T_Σ_14 → T_Dec_20 Source #
du_'215''45'decidable_222 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → T_Σ_14 → T_Σ_14 → T_Dec_20 Source #
d_'215''45'isEquivalence_236 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_28 → T_IsEquivalence_28 → T_IsEquivalence_28 Source #
du_'215''45'isEquivalence_236 ∷ T_IsEquivalence_28 → T_IsEquivalence_28 → T_IsEquivalence_28 Source #
d_'215''45'isDecEquivalence_250 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #
du_'215''45'isDecEquivalence_250 ∷ T_IsDecEquivalence_48 → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #
d_'215''45'isPreorder_260 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPreorder_76 → T_IsPreorder_76 → T_IsPreorder_76 Source #
d_'215''45'isPartialOrder_274 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsPartialOrder_248 → T_IsPartialOrder_248 → T_IsPartialOrder_248 Source #
du_'215''45'isPartialOrder_274 ∷ T_IsPartialOrder_248 → T_IsPartialOrder_248 → T_IsPartialOrder_248 Source #
d_'215''45'isStrictPartialOrder_288 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
du_'215''45'isStrictPartialOrder_288 ∷ T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_'215''45'setoid_304 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 Source #
d_'215''45'decSetoid_314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_DecSetoid_90 → T_DecSetoid_90 → T_DecSetoid_90 Source #
d_'215''45'preorder_324 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_142 → T_Preorder_142 → T_Preorder_142 Source #
d_'215''45'poset_334 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Poset_492 → T_Poset_492 Source #
d_'215''45'strictPartialOrder_344 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_StrictPartialOrder_760 → T_StrictPartialOrder_760 → T_StrictPartialOrder_760 Source #
du_'215''45'strictPartialOrder_344 ∷ T_StrictPartialOrder_760 → T_StrictPartialOrder_760 → T_StrictPartialOrder_760 Source #
d__'215''8347'__354 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 Source #
d_'8801''215''8801''8658''8801'_356 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T_Σ_14 → T__'8801'__12 Source #
d_'8801''8658''8801''215''8801'_358 ∷ T_Level_18 → () → T_Level_18 → () → T_Σ_14 → T_Σ_14 → T__'8801'__12 → T_Σ_14 Source #
d_Pointwise'45''8801''8596''8801'_360 ∷ T_Level_18 → () → T_Level_18 → () → T_Inverse_2122 Source #