:= comme un operateur particulier

parent dd5bc11a
...@@ -198,6 +198,8 @@ expr: ...@@ -198,6 +198,8 @@ expr:
{ $1 } { $1 }
| expr EQUAL expr | expr EQUAL expr
{ mk_infix $1 "=" $3 } { mk_infix $1 "=" $3 }
| expr COLONEQUAL expr
{ mk_infix $1 ":=" $3 }
| expr OP0 expr | expr OP0 expr
{ mk_infix $1 $2 $3 } { mk_infix $1 $2 $3 }
| expr OP1 expr | expr OP1 expr
......
...@@ -17,8 +17,9 @@ let p = ...@@ -17,8 +17,9 @@ let p =
assume { true -> old(!z) = 2 }; assume { true -> old(!z) = 2 };
while !x >= 0 do while !x >= 0 do
invariant { true } variant { t } invariant { true } variant { t }
() x := 2
done; done;
(* for x in s do () done; *)
f !x f !x
{ {
......
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