Idris2Doc : Frexlet.Monoid.Theory

Frexlet.Monoid.Theory

The syntax and axioms for monoids

Definitions

dataOperation : Nat->Type
Totality: total
Visibility: public export
Constructors:
Neutral : Operation0
Product : Operation2
Signature : Signature
Totality: total
Visibility: public export
dataAxiom : Type
Totality: total
Visibility: public export
Constructors:
LftNeutrality : Axiom
RgtNeutrality : Axiom
Associativity : Axiom

Hint: 
FiniteAxiom
MonoidTheory : Presentation
Totality: total
Visibility: public export
MonoidStructure : Type
Totality: total
Visibility: public export
Monoid : Type
Totality: total
Visibility: public export
Unit : OpSignature
Totality: total
Visibility: public export
Prod : OpSignature
Totality: total
Visibility: public export
ascii : PrinterSignature ()
Totality: total
Visibility: export
generic : PrinterSignature ()
Totality: total
Visibility: export
natPlus : PrinterSignature ()
Totality: total
Visibility: export
additive1 : PrinterSignature ()
Totality: total
Visibility: export
additive2 : PrinterSignature ()
Totality: total
Visibility: export
withRaw : PrinterSignaturea->PrinterMonoidTheorya
Totality: total
Visibility: export
withWords : PrinterSignaturea->PrinterMonoidTheorya
Totality: total
Visibility: export