| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
Documentation
d__'8776'__22 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → () Source #
d__'8818'__26 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → () Source #
d_Associative_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Commutative_130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Congruent'8321'_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny) → () Source #
d_Congruent'8322'_134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Idempotent_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Identity_146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftIdentity_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftZero_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightIdentity_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightZero_210 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Selective_212 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Zero_230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_IsBand_242 ∷ p → p → p → p → p → p → () Source #
d_IsCommutativeSemigroup_266 ∷ p → p → p → p → p → p → () Source #
d_IsMagma_322 ∷ p → p → p → p → p → p → () Source #
d_IsMonoid_334 ∷ p → p → p → p → p → p → p → () Source #
d_IsSelectiveMagma_374 ∷ p → p → p → p → p → p → () Source #
d_IsSemigroup_378 ∷ p → p → p → p → p → p → () Source #
d_idem_506 ∷ T_IsBand_526 → AgdaAny → AgdaAny Source #
d_'8729''45'cong_1688 ∷ T_IsMagma_178 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_2530 ∷ T_IsSemigroup_488 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_2924 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_2924 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_2950 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_2950 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'comm_2972 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_2972 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_2998 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_2998 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_3036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_3036 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong_3046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_3046 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_3060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_3060 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_3100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny Source #
d_'8851''45'sel_3104 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_3104 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'identity'737'_3112 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'691'_3118 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity_3124 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'737'_3130 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'691'_3136 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero_3142 ∷ T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'isMagma_3146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_IsMagma_178 Source #
d_'8851''45'isSemigroup_3148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_IsSemigroup_488 Source #
du_'8851''45'isSemigroup_3148 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_IsSemigroup_488 Source #
d_'8851''45'isBand_3150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_IsBand_526 Source #
d_'8851''45'isCommutativeSemigroup_3152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_IsCommutativeSemigroup_568 Source #
du_'8851''45'isCommutativeSemigroup_3152 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_IsCommutativeSemigroup_568 Source #
d_'8851''45'isSelectiveMagma_3154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_IsSelectiveMagma_450 Source #
du_'8851''45'isSelectiveMagma_3154 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_IsSelectiveMagma_450 Source #
d_'8851''45'isMonoid_3158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
du_'8851''45'isMonoid_3158 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
d_'8851''45'rawMagma_3162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_RawMagma_44 Source #
d_'8851''45'magma_3164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_Magma_74 Source #
d_'8851''45'semigroup_3166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_Semigroup_558 Source #
d_'8851''45'band_3168 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_Band_620 Source #
d_'8851''45'commutativeSemigroup_3170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_CommutativeSemigroup_688 Source #
du_'8851''45'commutativeSemigroup_3170 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_CommutativeSemigroup_688 Source #
d_'8851''45'selectiveMagma_3172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → T_SelectiveMagma_130 Source #
du_'8851''45'selectiveMagma_3172 ∷ T_TotalPreorder_240 → T_MinOperator_106 → T_SelectiveMagma_130 Source #
d_'8851''45'monoid_3176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
du_'8851''45'monoid_3176 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
d_x'8851'y'8776'x'8658'x'8804'y_3184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_3184 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_3216 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_3216 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_mono'45''8804''45'distrib'45''8851'_3230 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8851'_3230 ∷ T_TotalPreorder_240 → T_MinOperator_106 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_3276 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_3276 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_3288 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_3288 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_3300 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_3300 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_3314 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_3314 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'45''8804'_3322 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_3322 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_3372 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_3372 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'691''45''8804'_3382 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_3382 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'glb_3394 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_3394 ∷ T_TotalPreorder_240 → T_MinOperator_106 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #