| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Construct.NaturalChoice.MinOp
Documentation
d__'8776'__22 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → () Source #
d__'8818'__24 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → () Source #
d_Associative_118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Commutative_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Congruent'8321'_124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny) → () Source #
d_Congruent'8322'_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Idempotent_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Identity_138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftIdentity_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_LeftZero_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightIdentity_194 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_RightZero_202 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Selective_204 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_Zero_222 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny → AgdaAny) → () Source #
d_IsBand_230 ∷ p → p → p → p → p → p → () Source #
d_IsCommutativeSemigroup_242 ∷ p → p → p → p → p → p → () Source #
d_IsMagma_270 ∷ p → p → p → p → p → p → () Source #
d_IsMonoid_276 ∷ p → p → p → p → p → p → p → () Source #
d_IsSelectiveMagma_296 ∷ p → p → p → p → p → p → () Source #
d_IsSemigroup_298 ∷ p → p → p → p → p → p → () Source #
d_idem_412 ∷ T_IsBand_508 → AgdaAny → AgdaAny Source #
d_'8729''45'cong_1584 ∷ T_IsMagma_176 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_assoc_2424 ∷ T_IsSemigroup_472 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_2808 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_2808 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_2834 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_2834 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'comm_2856 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_2856 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_2882 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_2882 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_2920 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_2920 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong_2930 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_2930 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_2944 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_2944 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_2984 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny Source #
d_'8851''45'sel_2988 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_2988 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'identity'737'_2996 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'691'_3002 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity_3008 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'737'_3014 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'691'_3020 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero_3026 ∷ T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'isMagma_3030 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_IsMagma_176 Source #
d_'8851''45'isSemigroup_3032 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_IsSemigroup_472 Source #
d_'8851''45'isBand_3034 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_IsBand_508 Source #
d_'8851''45'isCommutativeSemigroup_3036 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_IsCommutativeSemigroup_548 Source #
du_'8851''45'isCommutativeSemigroup_3036 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_IsCommutativeSemigroup_548 Source #
d_'8851''45'isSelectiveMagma_3038 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_IsSelectiveMagma_436 Source #
du_'8851''45'isSelectiveMagma_3038 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_IsSelectiveMagma_436 Source #
d_'8851''45'isMonoid_3042 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_686 Source #
du_'8851''45'isMonoid_3042 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_686 Source #
d_'8851''45'rawMagma_3046 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_RawMagma_36 Source #
d_'8851''45'magma_3048 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_Magma_68 Source #
d_'8851''45'semigroup_3050 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_Semigroup_536 Source #
d_'8851''45'band_3052 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_Band_596 Source #
d_'8851''45'commutativeSemigroup_3054 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_CommutativeSemigroup_662 Source #
du_'8851''45'commutativeSemigroup_3054 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_CommutativeSemigroup_662 Source #
d_'8851''45'selectiveMagma_3056 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → T_SelectiveMagma_122 Source #
du_'8851''45'selectiveMagma_3056 ∷ T_TotalPreorder_222 → T_MinOperator_98 → T_SelectiveMagma_122 Source #
d_'8851''45'monoid_3060 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_882 Source #
du_'8851''45'monoid_3060 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_882 Source #
d_x'8851'y'8776'x'8658'x'8804'y_3068 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_3068 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_3100 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_3100 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_mono'45''8804''45'distrib'45''8851'_3114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
du_mono'45''8804''45'distrib'45''8851'_3114 ∷ T_TotalPreorder_222 → T_MinOperator_98 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'x'8851'z'8804'y_3160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_3160 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_3172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_3172 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_3184 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_3184 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_3198 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_3198 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'45''8804'_3206 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_3206 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_3256 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_3256 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'691''45''8804'_3266 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_3266 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'glb_3278 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_3278 ∷ T_TotalPreorder_222 → T_MinOperator_98 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #