Commit 97232540 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre

Fix overloaded notation behaviour for offset addition.

parent d4d61110
......@@ -18,7 +18,8 @@ Next Obligation. done. Qed.
Definition loc_add (l : loc) (off : Z) : loc :=
{| loc_car := loc_car l + off|}.
Notation "l +ₗ off" := (loc_add l off) (at level 50, left associativity).
Notation "l +ₗ off" :=
(loc_add l off) (at level 50, left associativity) : stdpp_scope.
Lemma loc_add_assoc l i j : l + i + j = l + (i + j).
Proof. destruct l; rewrite /loc_add /=; f_equal; lia. Qed.
......
......@@ -32,7 +32,7 @@ Notation Skip := (App (Val $ LamV BAnon (Val $ LitV LitUnit)) (Val $ LitV LitUni
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
......
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