Skip to content

Commit

Permalink
Fixed typos
Browse files Browse the repository at this point in the history
  • Loading branch information
Junaid Babar committed Jan 30, 2025
1 parent 7c7bf2d commit dd39e99
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions isolette/rust-prototyping/isolette-rust-prototyping.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ Next step: consult Verus documentation for this.

Example from Verus documentation referring to the use of old for initial and final values of variables in functions: (https://verus-lang.github.io/verus/guide/induction.html#towards-an-imperative-implementation-mutation-and-tail-recursion)

Compiling the above verus contract without old produces the following error:
Compiling the above Verus contract without old produces the following error:
```
$ verus src/manage_heat_source.rs
error: in requires, use `old(self)` to refer to the pre-state of an &mut variable
Expand All @@ -40,7 +40,7 @@ error: in requires, use `old(self)` to refer to the pre-state of an &mut variabl
132 | self.api.lower_desired_temp <= self.api.upper_desired_temp
| ^^^^
```
As indicates in the error, "self" is a mutable variable in this function and thus requires the use of old(self) in the pre-condition.
As indicated in the error, "self" is a mutable variable in this function and thus requires the use of old(self) in the pre-condition.

This is confirmed by compiling the following:
```
Expand Down

0 comments on commit dd39e99

Please sign in to comment.