(-@) : Type -> Type -> Type
Infix notation for linear implication
Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 0id : 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 9record (!*) : 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