Commit 88f41ac7 authored by charguer's avatar charguer

inprogress

parent 64da8061
......@@ -134,10 +134,14 @@ Notation "\[]" := (hprop_empty)
Notation "\[ L ]" := (hprop_empty_st L)
(at level 0, L at level 99) : heap_scope.
Notation "r '~~>' v" := (hprop_single r v)
(at level 32, no associativity) : heap_scope.
Notation "H1 '\*' H2" := (hprop_star H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "\GC" := (hprop_gc) : heap_scope.
Notation "Q \*+ H" := (fun x => hprop_star (Q x) H)
(at level 40) : heap_scope.
Notation "'Hexists' x1 , H" := (hprop_exists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
......@@ -146,12 +150,7 @@ Notation "'Hexists' x1 : T1 , H" := (hprop_exists (fun x1:T1 => H))
Notation "'Hexists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "r '~~>' v" := (hprop_single r v)
(at level 32, no associativity) : heap_scope.
Notation "Q \*+ H" :=
(fun x => hprop_star (Q x) H)
(at level 40) : heap_scope.
Notation "\GC" := (hprop_gc) : heap_scope.
Notation "'\$' n" := (hprop_credits n)
(at level 40, format "\$ n") : heap_scope.
......
This diff is collapsed.
......@@ -80,7 +80,7 @@ Global Opaque hprop_empty hprop_empty_st hprop_single
Notation "\# h1 h2" := (heap_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : heap_scope.
Notation "\# h1 h2 h3" := (state_disjoint_3 h1 h2 h3)
Notation "\# h1 h2 h3" := (heap_disjoint_3 h1 h2 h3)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity) : heap_scope.
Notation "h1 \+ h2" := (heap_union h1 h2)
......@@ -102,8 +102,7 @@ Notation "r '~~>' v" := (hprop_single r v)
Notation "H1 '\*' H2" := (hprop_star H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" :=
(fun x => hprop_star (Q x) H)
Notation "Q \*+ H" := (fun x => hprop_star (Q x) H)
(at level 40) : heap_scope.
Notation "'Hexists' x1 , H" := (hprop_exists (fun x1 => H))
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment