Data.Linear.Notation

Definitions

(-@) : Type -> Type -> Type

  Infix notation for linear implication

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 0

id : a -@ a

  Linear identity function

Totality: total
Visibility: public export

(.) : (b -@ c) -@ ((a -@ b) -@ (a -@ c))

  Linear function composition

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 9

record (!*) : Type -> Type

  Prefix notation for the linear unrestricted modality

Totality: total
Visibility: public export
Constructor: 

MkBang : a -> (!*) a

Projection: 

.unrestricted : (!*) a -> a

Hints:

Comonoid ((!*) a)

Consumable ((!*) a)

Duplicable ((!*) a)

Fixity Declaration: prefix operator, level 5

.unrestricted : (!*) a -> a

Totality: total
Visibility: public export

unrestricted : (!*) a -> a

Totality: total
Visibility: public export