Idris2Doc : Frexlet.Monoid.Commutative.Notation.Core

Frexlet.Monoid.Commutative.Notation.Core

Notational conventions for commutative monoid

Reexports

import public Notation
import public Notation.Action
import public Data.Vect.Quantifiers
import public Frex.Free
import public Frex.Free.Construction

Definitions

cast : (a : MonoidStructure) -> HVect [ary 0 (U a), ary 2 (U a)]
Totality: total
Visibility: public export
cast : (a : CommutativeMonoid) -> HVect [ary 0 (U a), ary 2 (U a)]
Totality: total
Visibility: public export
.sum : (a : CommutativeMonoid) -> Vect n (U a) -> U a
Totality: total
Visibility: public export
mult : (a : CommutativeMonoid) -> Nat -> U a -> U a
Totality: total
Visibility: public export
NatActionData : (a : CommutativeMonoid) -> ActionData Nat (U a)
Totality: total
Visibility: public export
NatAction1 : (a : CommutativeMonoid) -> Action1 Nat (U a)
Totality: total
Visibility: public export
NatAction2 : (a : CommutativeMonoid) -> Action2 Nat (U a)
Totality: total
Visibility: public export
notation2 : Action2 Nat (Term Signature (Either a (Fin n)))
Totality: total
Visibility: public export
notation1 : Action1 Nat (Term Signature (Either a (Fin n)))
Totality: total
Visibility: public export