Frexlet.Monoid.Free

Definitions

TrivialAlgebra : Algebra Signature

  The trivial algebra with carrier the unit type

Totality: total
Visibility: public export

TrivialMonoid : Monoid

  The trivial monoid with carrier the unit type

Totality: total
Visibility: public export

FreeMonoidVoid : Free MonoidTheory (cast Void)

  The free monoid (over the empty setoid) is the trivial monoid

Totality: total
Visibility: public export

FreeMonoidOver : (s : Setoid) -> Free MonoidTheory s

Totality: total
Visibility: public export

FreeMonoid : Nat -> Monoid

  A free monoid built out of n variables

Totality: total
Visibility: public export

SyntacticFrex : (n : Nat) -> Frex (FreeMonoid n) (cast (Fin 0))

Totality: total
Visibility: public export

SyntacticExtension : (n : Nat) -> Extension (FreeMonoid n) (cast (Fin 0))

Totality: total
Visibility: public export

SyntacticMonoid : Nat -> Monoid

Totality: total
Visibility: public export