pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix goofy notation

Browse source
This commit is contained in:
Adam Chlipala 2016-02-28 20:18:29 -05:00
parent ce0d9e8262
commit 64516f784a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
OperationalSemantics.v
View file

@ -37,7 +37,7 @@ Infix "*" := Times : arith_scope.
Delimit Scope arith_scope with arith. Delimit Scope arith_scope with arith.
Notation "x <- e" := (Assign x e%arith) (at level 75). Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *) Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *)
Notation "'when' e 'loop' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0). Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0).
Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75). Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75).
(* Here's an adaptation of our factorial example from Chapter 3. *) (* Here's an adaptation of our factorial example from Chapter 3. *)
@ -974,7 +974,7 @@ Module Concurrent.
Notation "x <- e" := (Assign x e%arith) (at level 75). Notation "x <- e" := (Assign x e%arith) (at level 75).
Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *) Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *)
Notation "'when' e 'loop' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0). Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0).
Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75). Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75).
Infix "||" := Parallel. Infix "||" := Parallel.