Frexlet.Monoid.Theory

The syntax and axioms for monoids

Definitions

data Operation : Nat -> Type

Totality: total
Visibility: public export
Constructors:

Neutral : Operation 0

Product : Operation 2

Signature : Signature

Totality: total
Visibility: public export

data Axiom : Type

Totality: total
Visibility: public export
Constructors:

LftNeutrality : Axiom

RgtNeutrality : Axiom

Associativity : Axiom

Hint: 

Finite Axiom

MonoidTheory : Presentation

Totality: total
Visibility: public export

MonoidStructure : Type

Totality: total
Visibility: public export

Monoid : Type

Totality: total
Visibility: public export

Unit : Op Signature

Totality: total
Visibility: public export

Prod : Op Signature

Totality: total
Visibility: public export

ascii : Printer Signature ()

Totality: total
Visibility: export

generic : Printer Signature ()

Totality: total
Visibility: export

natPlus : Printer Signature ()

Totality: total
Visibility: export

additive1 : Printer Signature ()

Totality: total
Visibility: export

additive2 : Printer Signature ()

Totality: total
Visibility: export

withRaw : Printer Signature a -> Printer MonoidTheory a

Totality: total
Visibility: export

withWords : Printer Signature a -> Printer MonoidTheory a

Totality: total
Visibility: export