| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Data.Sum.Relation.Binary.Pointwise
Documentation
d_Pointwise_70 ∷ p → p → p → p → p → p → p → p → p → p → p → p → p → p → () Source #
data T_Pointwise_70 Source #
Constructors
| C_inj'8321'_88 AgdaAny | |
| C_inj'8322'_94 AgdaAny |
d_map_100 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_map_100 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d_drop'45'inj'8321'_114 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Pointwise_70 → AgdaAny Source #
d_drop'45'inj'8322'_122 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → AgdaAny → AgdaAny → T_Pointwise_70 → AgdaAny Source #
d_'8846''45'refl_126 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_70 Source #
du_'8846''45'refl_126 ∷ (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny) → T__'8846'__30 → T_Pointwise_70 Source #
d_'8846''45'symmetric_140 ∷ 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__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'8846''45'symmetric_140 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'8846''45'transitive_154 ∷ 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__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'8846''45'transitive_154 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'8846''45'asymmetric_172 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Irrelevant_20 Source #
d_'46'extendedlambda0_180 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_70 → T_Irrelevant_20 Source #
d_'46'extendedlambda1_190 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → AgdaAny → AgdaAny → AgdaAny → T_Pointwise_70 → T_Irrelevant_20 Source #
d_'8846''45'substitutive_194 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (T__'8846'__30 → ()) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → AgdaAny → AgdaAny Source #
du_'8846''45'substitutive_194 ∷ ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → ((AgdaAny → ()) → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (T__'8846'__30 → ()) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → AgdaAny → AgdaAny Source #
d_'8846''45'decidable_212 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → T__'8846'__30 → T__'8846'__30 → T_Dec_20 Source #
du_'8846''45'decidable_212 ∷ (AgdaAny → AgdaAny → T_Dec_20) → (AgdaAny → AgdaAny → T_Dec_20) → T__'8846'__30 → T__'8846'__30 → T_Dec_20 Source #
d_'8846''45'reflexive_246 ∷ 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__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'8846''45'reflexive_246 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'8846''45'irreflexive_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 → ()) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → T_Irrelevant_20) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Irrelevant_20 Source #
d_'8846''45'antisymmetric_278 ∷ 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__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'8846''45'antisymmetric_278 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'8846''45'respects'737'_296 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → 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__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'8846''45'respects'737'_296 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'8846''45'respects'691'_314 ∷ T_Level_18 → () → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → 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__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
du_'8846''45'respects'691'_314 ∷ (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Pointwise_70 → T_Pointwise_70 Source #
d_'8846''45'respects'8322'_332 ∷ 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_'8846''45'isEquivalence_342 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsEquivalence_26 → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
du_'8846''45'isEquivalence_342 ∷ T_IsEquivalence_26 → T_IsEquivalence_26 → T_IsEquivalence_26 Source #
d_'8846''45'isDecEquivalence_352 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
du_'8846''45'isDecEquivalence_352 ∷ T_IsDecEquivalence_44 → T_IsDecEquivalence_44 → T_IsDecEquivalence_44 Source #
d_'8846''45'isPreorder_362 ∷ 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_70 → T_IsPreorder_70 → T_IsPreorder_70 Source #
d_'8846''45'isPartialOrder_372 ∷ 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_174 → T_IsPartialOrder_174 → T_IsPartialOrder_174 Source #
du_'8846''45'isPartialOrder_372 ∷ T_IsPartialOrder_174 → T_IsPartialOrder_174 → T_IsPartialOrder_174 Source #
d_'8846''45'isStrictPartialOrder_382 ∷ 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_290 → T_IsStrictPartialOrder_290 → T_IsStrictPartialOrder_290 Source #
du_'8846''45'isStrictPartialOrder_382 ∷ T_IsStrictPartialOrder_290 → T_IsStrictPartialOrder_290 → T_IsStrictPartialOrder_290 Source #
d_'8846''45'setoid_392 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #
d_'8846''45'decSetoid_402 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_DecSetoid_84 → T_DecSetoid_84 → T_DecSetoid_84 Source #
d_'8846''45'preorder_412 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Preorder_132 → T_Preorder_132 → T_Preorder_132 Source #
d_'8846''45'poset_422 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_314 → T_Poset_314 → T_Poset_314 Source #
d__'8846''8347'__432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_44 → T_Setoid_44 → T_Setoid_44 Source #
d_Pointwise'45''8801''8658''8801'_434 ∷ T_Level_18 → () → T_Level_18 → () → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T__'8801'__12 Source #
d_'8801''8658'Pointwise'45''8801'_440 ∷ T_Level_18 → () → T_Level_18 → () → T__'8846'__30 → T__'8846'__30 → T__'8801'__12 → T_Pointwise_70 Source #
d_Pointwise'45''8801''8596''8801'_446 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_1960 Source #