Idris2Doc : Data.Linear.Notation

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