Commit 457c12fe authored by Robbert Krebbers's avatar Robbert Krebbers

Make some overlapping heap_lang notations parsing only.

parent 6e697ccc
...@@ -91,15 +91,15 @@ Notation "e1 || e2" := ...@@ -91,15 +91,15 @@ Notation "e1 || e2" :=
(If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope. (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
(** Notations for option *) (** Notations for option *)
Notation NONE := (InjL #()). Notation NONE := (InjL #()) (only parsing).
Notation SOME x := (InjR x). Notation SOME x := (InjR x) (only parsing).
Notation NONEV := (InjLV #()). Notation NONEV := (InjLV #()) (only parsing).
Notation SOMEV x := (InjRV x). Notation SOMEV x := (InjRV x) (only parsing).
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" := Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
(Match e0 BAnon e1 x%bind e2) (Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200) : expr_scope. (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" := Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%bind e2) (Match e0 BAnon e1 x%bind e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope. (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
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