Idris2Doc : Notation.Action

Notation.Action

Reexports
import public Data.Vect.Quantifiers
import public Data.Fun.Extra
import public Notation
import public Notation.Additive
import public Notation.Multiplicative
Definitions
Action1 : Type -> Type -> Type
  Totality: total
  Visibility: public export
Action2 : Type -> Type -> Type
  Totality: total
  Visibility: public export
Action3 : Type -> Type -> Type
  Totality: total
  Visibility: public export
MAction1 : Type -> Type -> Type
  Totality: total
  Visibility: public export
MAction2 : Type -> Type -> Type
  Totality: total
  Visibility: public export
MAction3 : Type -> Type -> Type
  Totality: total
  Visibility: public export
ActionData : Type -> Type -> Type
  Totality: total
  Visibility: public export