Commit ee8c4875 authored by Robbert Krebbers's avatar Robbert Krebbers

Right associativity of some heap_lang constructs.

parent 87e70e92
......@@ -20,9 +20,11 @@ Coercion of_val : val >-> expr.
(* What about Arguments for hoare triples?. *)
Notation "' l" := (Lit l) (at level 8, format "' l") : lang_scope.
Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
Notation "- e" := (UnOp MinusUnOp e%L) (at level 35, right associativity) : lang_scope.
Notation "! e" := (Load e%L) (at level 10, right associativity) : lang_scope.
Notation "'ref' e" := (Alloc e%L)
(at level 30, right associativity) : lang_scope.
Notation "- e" := (UnOp MinusUnOp e%L)
(at level 35, right associativity) : lang_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
(at level 50, left associativity) : lang_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
......
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