notation.v 4.74 KB
Newer Older
1
(** Just reserve the notation. *)
Ralf Jung's avatar
Ralf Jung committed
2
3

(** Turnstiles *)
4
5
6
7
8
9
Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
Reserved Notation "('⊢@{' PROP } )" (at level 99).
Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
Ralf Jung's avatar
Ralf Jung committed
10
11

(** BI connectives *)
12
13
14
Reserved Notation "'emp'".
Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
Reserved Notation "P ∗ Q" (at level 80, right associativity).
15
16
17
Reserved Notation "P -∗ Q"
  (at level 99, Q at level 200, right associativity,
   format "'[' P  '/' -∗  Q ']'").
18

Ralf Jung's avatar
Ralf Jung committed
19
20
Reserved Notation "⎡ P ⎤".

Ralf Jung's avatar
Ralf Jung committed
21
(** Modalities *)
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
Reserved Notation "'<pers>' P" (at level 20, right associativity).
Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<pers>?' p  P").

Reserved Notation "▷ P" (at level 20, right associativity).
Reserved Notation "▷? p P" (at level 20, p at level 9, P at level 20,
   format "▷? p  P").
Reserved Notation "▷^ n P" (at level 20, n at level 9, P at level 20,
   format "▷^ n  P").

Reserved Infix "∗-∗" (at level 95, no associativity).

Reserved Notation "'<affine>' P" (at level 20, right associativity).
Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'<affine>?' p  P").

Reserved Notation "'<absorb>' P" (at level 20, right associativity).

Reserved Notation "□ P" (at level 20, right associativity).
Reserved Notation "'□?' p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "'□?' p  P").

Reserved Notation "◇ P" (at level 20, right associativity).

Reserved Notation "■ P" (at level 20, right associativity).
Reserved Notation "■? p P" (at level 20, p at level 9, P at level 20,
   right associativity, format "■? p  P").

Ralf Jung's avatar
Ralf Jung committed
50
51
52
Reserved Notation "'<obj>' P" (at level 20, right associativity).
Reserved Notation "'<subj>' P" (at level 20, right associativity).

Ralf Jung's avatar
Ralf Jung committed
53
(** Update modalities *)
54
Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
55
Reserved Notation "P ==∗ Q"
56
  (at level 99, Q at level 200, format "'[' P  '/' ==∗  Q ']'").
57

Ralf Jung's avatar
Ralf Jung committed
58
59
60
61
62
Reserved Notation "|={ E1 , E2 }=> Q"
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }=>  Q").
Reserved Notation "P ={ E1 , E2 }=∗ Q"
  (at level 99, E1,E2 at level 50, Q at level 200,
63
   format "'[' P  '/' ={ E1 , E2 }=∗  Q ']'").
Ralf Jung's avatar
Ralf Jung committed
64
65
66
67
68
69

Reserved Notation "|={ E }=> Q"
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }=>  Q").
Reserved Notation "P ={ E }=∗ Q"
  (at level 99, E at level 50, Q at level 200,
70
   format "'[' P  '/' ={ E }=∗  Q ']'").
Ralf Jung's avatar
Ralf Jung committed
71
72
73
74
75
76

Reserved Notation "|={ E1 , E2 }▷=> Q"
  (at level 99, E1, E2 at level 50, Q at level 200,
   format "|={ E1 , E2 }▷=>  Q").
Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
  (at level 99, E1, E2 at level 50, Q at level 200,
77
   format "'[' P  '/' ={ E1 , E2 }▷=∗  Q ']'").
Ralf Jung's avatar
Ralf Jung committed
78
79
80
81
82
Reserved Notation "|={ E }▷=> Q"
  (at level 99, E at level 50, Q at level 200,
   format "|={ E }▷=>  Q").
Reserved Notation "P ={ E }▷=∗ Q"
  (at level 99, E at level 50, Q at level 200,
83
   format "'[' P  '/' ={ E }▷=∗  Q ']'").
Ralf Jung's avatar
Ralf Jung committed
84

Ralf Jung's avatar
Ralf Jung committed
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
(** Big Ops *)
Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
  (at level 200, l at level 10, k, x at level 1, right associativity,
   format "[∗  list]  k ↦ x  ∈  l ,  P").
Reserved Notation "'[∗' 'list]' x ∈ l , P"
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[∗  list]  x  ∈  l ,  P").

Reserved Notation "'[∗]' Ps" (at level 20).

Reserved Notation "'[∧' 'list]' k ↦ x ∈ l , P"
  (at level 200, l at level 10, k, x at level 1, right associativity,
   format "[∧  list]  k ↦ x  ∈  l ,  P").
Reserved Notation "'[∧' 'list]' x ∈ l , P"
  (at level 200, l at level 10, x at level 1, right associativity,
   format "[∧  list]  x  ∈  l ,  P").

Reserved Notation "'[∧]' Ps" (at level 20).

Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
  (at level 200, m at level 10, k, x at level 1, right associativity,
   format "[∗  map]  k ↦ x  ∈  m ,  P").
Reserved Notation "'[∗' 'map]' x ∈ m , P"
  (at level 200, m at level 10, x at level 1, right associativity,
   format "[∗  map]  x  ∈  m ,  P").

Reserved Notation "'[∗' 'set]' x ∈ X , P"
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[∗  set]  x  ∈  X ,  P").

Reserved Notation "'[∗' 'mset]' x ∈ X , P"
  (at level 200, X at level 10, x at level 1, right associativity,
   format "[∗  mset]  x  ∈  X ,  P").

119
120
(** Define the scope *)
Delimit Scope bi_scope with I.