Skip to content

Commit

Permalink
docs: explicitly show implication operator ==> when introducing it
Browse files Browse the repository at this point in the history
  • Loading branch information
das-g committed Nov 27, 2024
1 parent fb91dc2 commit d341a73
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion docs/OnlineTutorial/guide.md
Original file line number Diff line number Diff line change
Expand Up @@ -516,7 +516,7 @@ method Abs(x: int) returns (y: int)

This expresses exactly the property we discussed before,
that the absolute value is the same for non-negative integers. The second
ensures is expressed via the implication operator, which basically says that
ensures is expressed via the implication operator `==>`, which basically says that
the left hand side implies the right in the mathematical sense (it binds more
weakly than boolean "and" and comparisons, so the above says `0 <= x` implies `y == x`).
The left and right sides must both be boolean expressions.
Expand Down

0 comments on commit d341a73

Please sign in to comment.