Skip to content
Snippets Groups Projects
Commit e4975c8b authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Put the shift_loc notation in the right scope so that it is parsed/printed...

Put the shift_loc notation in the right scope so that it is parsed/printed properly even when appearing in expressions.
parent adec152c
No related branches found
No related tags found
No related merge requests found
......@@ -198,7 +198,8 @@ Definition lit_of_bool (b : bool) : base_lit :=
Definition shift_loc (l : loc) (z : Z) : loc := (l.1, l.2 + z).
Notation "l +ₗ z" := (shift_loc l%L z%Z) (at level 50, left associativity).
Notation "l +ₗ z" := (shift_loc l%L z%Z)
(at level 50, left associativity) : loc_scope.
Fixpoint init_mem (l:loc) (init:list val) (σ:state) : state :=
match init with
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment