| 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'wellFounded_278 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → T_Acc_42) → T__'8846'__30 → T_Acc_42 Source #
d_'8846''45'acc'8321'_296 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → T_Acc_42) → T__'8846'__30 → AgdaAny → T_Acc_42 → T__'8846'__30 → T_Pointwise_70 → T_Acc_42 Source #
d_'8846''45'acc'8322'_304 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → T_Acc_42) → T__'8846'__30 → AgdaAny → T_Acc_42 → T__'8846'__30 → T_Pointwise_70 → T_Acc_42 Source #
d_'8846''45'acc_312 ∷ T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → T_Level_18 → () → T_Level_18 → (AgdaAny → AgdaAny → ()) → (AgdaAny → T_Acc_42) → (AgdaAny → T_Acc_42) → T__'8846'__30 → T__'8846'__30 → T__'8846'__30 → T_Pointwise_70 → T_Acc_42 Source #
d_'8846''45'antisymmetric_318 ∷ 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_318 ∷ (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'_336 ∷ 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'_336 ∷ (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'_354 ∷ 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'_354 ∷ (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'_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_Σ_14 → T_Σ_14 → T_Σ_14 Source #
d_'8846''45'isEquivalence_382 ∷ 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_'8846''45'isEquivalence_382 ∷ T_IsEquivalence_28 → T_IsEquivalence_28 → T_IsEquivalence_28 Source #
d_'8846''45'isDecEquivalence_392 ∷ 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_'8846''45'isDecEquivalence_392 ∷ T_IsDecEquivalence_48 → T_IsDecEquivalence_48 → T_IsDecEquivalence_48 Source #
d_'8846''45'isPreorder_402 ∷ 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_'8846''45'isPartialOrder_412 ∷ 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_'8846''45'isPartialOrder_412 ∷ T_IsPartialOrder_248 → T_IsPartialOrder_248 → T_IsPartialOrder_248 Source #
d_'8846''45'isStrictPartialOrder_422 ∷ 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_'8846''45'isStrictPartialOrder_422 ∷ T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 → T_IsStrictPartialOrder_370 Source #
d_'8846''45'setoid_432 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 Source #
d_'8846''45'decSetoid_442 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_DecSetoid_90 → T_DecSetoid_90 → T_DecSetoid_90 Source #
d_'8846''45'preorder_452 ∷ 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_'8846''45'poset_462 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Poset_492 → T_Poset_492 → T_Poset_492 Source #
d__'8846''8347'__472 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_Level_18 → T_Setoid_46 → T_Setoid_46 → T_Setoid_46 Source #
d_Pointwise'45''8801''8658''8801'_474 ∷ 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'_480 ∷ 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'_486 ∷ T_Level_18 → T_Level_18 → () → () → T_Inverse_2122 Source #