notation.v 4.72 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
15
16
Reserved Notation "'emp'".
Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
Reserved Notation "P ∗ Q" (at level 80, right associativity).
Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).

Ralf Jung's avatar
Ralf Jung committed
17
18
Reserved Notation "⎡ P ⎤".

Ralf Jung's avatar
Ralf Jung committed
19
(** Modalities *)
20
21
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
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
48
49
50
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
51
(** Update modalities *)
52
Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
53
Reserved Notation "P ==∗ Q"
54
  (at level 99, Q at level 200, format "'[  ' P  ==∗  '/' Q ']'").
55

Ralf Jung's avatar
Ralf Jung committed
56
57
58
59
60
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,
61
   format "'[  ' P  ={ E1 , E2 }=∗  '/' Q ']'").
Ralf Jung's avatar
Ralf Jung committed
62
63
64
65
66
67

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,
68
   format "'[  ' P  ={ E }=∗  '/' Q ']'").
Ralf Jung's avatar
Ralf Jung committed
69
70
71
72
73
74

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,
75
   format "'[  ' P  ={ E1 , E2 }▷=∗  '/' Q ']'").
Ralf Jung's avatar
Ralf Jung committed
76
77
78
79
80
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,
81
   format "'[  ' P  ={ E }▷=∗  '/' Q ']'").
Ralf Jung's avatar
Ralf Jung committed
82

Ralf Jung's avatar
Ralf Jung committed
83
84
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
(** 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").

117
118
(** Define the scope *)
Delimit Scope bi_scope with I.