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

data (!*) : Type -> Type

  Prefix notation for the linear unrestricted modality

Totality: total
Visibility: public export
Constructor: 

MkBang : a -> (!*) a

Hints:

Comonoid ((!*) a)

Consumable ((!*) a)

Duplicable ((!*) a)

Fixity Declaration: prefix operator, level 5

unrestricted : (!*) a -@ a

  Unpack an unrestricted value in a linear context

Totality: total
Visibility: public export

.unrestricted : (!*) a -@ a

  Unpack an unrestricted value in a linear context
  
  A postfix alias for function unrestricted.

Totality: total
Visibility: public export