Skip to content

Commit

Permalink
Style fix in guide (#700)
Browse files Browse the repository at this point in the history
* Update modes.rs
  • Loading branch information
ahuoguo authored Jul 25, 2023
1 parent 2dc6a17 commit cd332f0
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions source/rust_verify/example/guide/modes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -350,22 +350,22 @@ fn test(s: S) {
*/

// ANCHOR: const1
spec const spec_one: int = 1;
spec const SPEC_ONE: int = 1;

spec fn spec_add_one(x: int) -> int {
x + spec_one
x + SPEC_ONE
}


const one: u8 = 1;
const ONE: u8 = 1;

fn add_one(x: u8) -> (ret: u8)
requires
x < 0xff,
ensures
ret == x + one // use "one" in spec code
ret == x + ONE // use "ONE" in spec code
{
x + one // use "one" in exec code
x + ONE // use "ONE" in exec code
}
// ANCHOR_END: const1

Expand Down

0 comments on commit cd332f0

Please sign in to comment.