Idris2Doc : Frexlet.Monoid.Notation.Multiplicative

Frexlet.Monoid.Notation.Multiplicative

Multiplicative notation for working with monoids (mostly boilerplate)

Reexports

import public Notation.Multiplicative

.Multiplicative1 : (monoid : Monoid) -> Multiplicative1 (U monoid): Totality: total
Visibility: public export
.Multiplicative2 : (monoid : Monoid) -> Multiplicative2 (U monoid): Totality: total
Visibility: public export
.Multiplicative3 : (monoid : Monoid) -> Multiplicative3 (U monoid): Totality: total
Visibility: public export
notationSyntax : Multiplicative1 (Term Signature x): Totality: total
Visibility: public export
notation1 : Multiplicative1 (Term Signature x): Totality: total
Visibility: public export
notation2 : Multiplicative2 (Term Signature x): Totality: total
Visibility: public export
notation3 : Multiplicative3 (Term Signature x): Totality: total
Visibility: public export