0 | module Data.Linear.Notation
 1 |
 2 | %default total
 3 |
 4 | export infixr 0 -@
 5 | ||| Infix notation for linear implication
 6 | public export
 7 | (-@) : Type -> Type -> Type
 8 | a -@ b = (1 _ : a) -> b
 9 |
10 | ||| Linear identity function
11 | public export
12 | id : a -@ a
13 | id x = x
14 |
15 | ||| Linear function composition
16 | public export
17 | (.) : (b -@ c) -@ (a -@ b) -@ (a -@ c)
18 | (.) f g v = f (g v)
19 |
20 | export prefix 5 !*
21 | ||| Prefix notation for the linear unrestricted modality
22 | public export
23 | data (!*) : Type -> Type where
24 |   MkBang : a -> !* a
25 |
26 | ||| Unpack an unrestricted value in a linear context
27 | public export
28 | unrestricted : !* a -@ a
29 | unrestricted (MkBang unr) = unr
30 |
31 | ||| Unpack an unrestricted value in a linear context
32 | |||
33 | ||| A postfix alias for function unrestricted.
34 | public export
35 | (.unrestricted) : !* a -@ a
36 | (.unrestricted) = unrestricted
37 |