Skip to content

Commit

Permalink
Update 'assuming' syntax in user doc
Browse files Browse the repository at this point in the history
  • Loading branch information
daniel-larraz committed May 15, 2024
1 parent 78a1b0b commit be1d05e
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions doc/usr/source/2_input/1_lustre.rst
Original file line number Diff line number Diff line change
Expand Up @@ -1115,7 +1115,7 @@ Because of this limitation, some checks may fail even if,
in a broader context where all constraints included in
the model are considered, the imported node would actually be considered
realizable. To mitigate this issue, Kind 2 offers an extended version of
the binder, ``any { x: T | P(x) assuming Q }``, that
the binder, ``any { x: T | P(x) } assuming { Q }``, that
allows the user to specify an assumption ``Q`` that
should be taken into account in the realizability check.
For instance, the realizability check for the ``any`` expression
Expand All @@ -1128,7 +1128,7 @@ was not included.
var b: int;
let
b = a + 10;
z = any { x: int | a <= x and x <= b assuming a<=b };
z = any { x: int | a <= x and x <= b } assuming { a<=b };
check z>=a+10 => z=b;
tel
Expand Down

0 comments on commit be1d05e

Please sign in to comment.