Frexlet.Monoid.Commutative.Theory

The syntax and axioms for monoids

Reexports

Definitions

data Axiom : Type

Totality: total
Visibility: public export
Constructors:

Mon : Axiom -> Axiom

Commutativity : Axiom

Hint: 

Finite Axiom

CommutativeMonoidTheory : Presentation

Totality: total
Visibility: public export

CommutativeMonoid : Type

Totality: total
Visibility: public export

MkCommutativeMonoid : (monoid : Monoid) -> ValidatesEquation (commutativity Product) (monoid .Algebra) -> CommutativeMonoid

  Smart constructor for commutative monoids

Totality: total
Visibility: public export

Zero : Op Signature

Totality: total
Visibility: public export

Plus : Op Signature

Totality: total
Visibility: public export

withRaw : Printer Signature a -> Printer CommutativeMonoidTheory a

Totality: total
Visibility: export

withWords : Printer Signature a -> Printer CommutativeMonoidTheory a

Totality: total
Visibility: export