| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
MAlonzo.Code.Algebra.Construct.NaturalChoice.MaxOp
Documentation
d__'8776'__30 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → () Source #
d__'8818'__34 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → () Source #
d_x'8804'y'8658'x'8851'z'8804'y_106 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'x'8851'z'8804'y_106 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8658'z'8851'x'8804'y_108 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8658'z'8851'x'8804'y_108 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'y_110 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'y_110 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8804'y'8851'z'8658'x'8804'z_112 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8804'y'8851'z'8658'x'8804'z_112 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'x'8658'x'8804'y_114 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'x'8658'x'8804'y_114 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8776'y'8658'y'8804'x_116 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8776'y'8658'y'8804'x_116 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'x_118 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'x_118 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_x'8851'y'8804'y_120 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_x'8851'y'8804'y_120 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'assoc_122 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'assoc_122 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'band_124 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_Band_620 Source #
d_'8851''45'comm_126 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'comm_126 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'commutativeSemigroup_128 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_CommutativeSemigroup_688 Source #
du_'8851''45'commutativeSemigroup_128 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_CommutativeSemigroup_688 Source #
d_'8851''45'cong_130 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong_130 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'691'_132 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'691'_132 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'cong'737'_134 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'cong'737'_134 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'glb_136 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'glb_136 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'idem_138 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny Source #
d_'8851''45'identity_140 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'identity_140 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'identity'691'_142 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'691'_142 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'identity'737'_144 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'identity'737'_144 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'isBand_146 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_IsBand_526 Source #
d_'8851''45'isCommutativeSemigroup_148 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_IsCommutativeSemigroup_568 Source #
du_'8851''45'isCommutativeSemigroup_148 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_IsCommutativeSemigroup_568 Source #
d_'8851''45'isMagma_150 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_IsMagma_178 Source #
d_'8851''45'isMonoid_152 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
du_'8851''45'isMonoid_152 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_IsMonoid_712 Source #
d_'8851''45'isSelectiveMagma_154 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_IsSelectiveMagma_450 Source #
du_'8851''45'isSelectiveMagma_154 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_IsSelectiveMagma_450 Source #
d_'8851''45'isSemigroup_156 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_IsSemigroup_488 Source #
d_'8851''45'magma_158 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_Magma_74 Source #
d_'8851''45'mono'45''8804'_160 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'45''8804'_160 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'monoid_162 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
du_'8851''45'monoid_162 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Monoid_914 Source #
d_'8851''45'mono'691''45''8804'_164 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'691''45''8804'_164 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'mono'737''45''8804'_166 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'mono'737''45''8804'_166 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'sel_170 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → T__'8846'__30 Source #
du_'8851''45'sel_170 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → T__'8846'__30 Source #
d_'8851''45'selectiveMagma_172 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_SelectiveMagma_130 Source #
du_'8851''45'selectiveMagma_172 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → T_SelectiveMagma_130 Source #
d_'8851''45'semigroup_174 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → T_Semigroup_558 Source #
d_'8851''45'triangulate_176 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
du_'8851''45'triangulate_176 ∷ T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → AgdaAny → AgdaAny → AgdaAny Source #
d_'8851''45'zero_178 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
du_'8851''45'zero_178 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → T_Σ_14 Source #
d_'8851''45'zero'691'_180 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'691'_180 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_'8851''45'zero'737'_182 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
du_'8851''45'zero'737'_182 ∷ T_MaxOperator_138 → AgdaAny → (AgdaAny → AgdaAny) → AgdaAny → AgdaAny Source #
d_mono'45''8804''45'distrib'45''8852'_190 ∷ T_Level_18 → T_Level_18 → T_Level_18 → T_TotalPreorder_240 → T_MaxOperator_138 → (AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → (AgdaAny → AgdaAny → AgdaAny → AgdaAny) → AgdaAny → AgdaAny → AgdaAny Source #