Skip to content

Commit 3bde981

Browse files
committed
Minor Change
1 parent 2a26eee commit 3bde981

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

diagnostics/structure.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ In the example above:
3535

3636
So the counterexample explains exactly why LiquidJava cannot prove that `x / 2` is always positive even when `x > 0`. To fix this error, we would need to either change the return expression to allow to return zero with the refinement `_ >= 0`, or strengthen the parameter refinement to require `x > 1`.
3737

38-
## Internal Instance Variables
38+
## Understanding Internal Variables
3939

4040
Names such as `#ret²` are internal variables introduced by LiquidJava during verification. The small superscript number is a counter used to keep those generated variables unique.
4141

0 commit comments

Comments
 (0)