Frexlet.Monoid.Notation.Additive

Additive notation for working with monoids (mostly boilerplate)

Reexports

Definitions

cast : (a : MonoidStructure) -> HVect [ary 0 (U a), ary 2 (U a)]

Totality: total
Visibility: public export

cast : (a : Monoid) -> HVect [ary 0 (U a), ary 2 (U a)]

Totality: total
Visibility: public export

.Additive1 : (monoid : Monoid) -> Additive1 (U monoid)

Totality: total
Visibility: public export

.Additive2 : (monoid : Monoid) -> Additive2 (U monoid)

Totality: total
Visibility: public export

.Additive3 : (monoid : Monoid) -> Additive3 (U monoid)

Totality: total
Visibility: public export

notationAdd1 : Additive1 (Term Signature x)

Totality: total
Visibility: public export

notationAdd2 : Additive2 (Term Signature x)

Totality: total
Visibility: public export

notationAdd3 : Additive3 (Term Signature x)

Totality: total
Visibility: public export