search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.25k stars 72 forks source link

Fix state machine example in book #1358

Closed suaviloquence closed 4 days ago

suaviloquence commented 4 days ago

Playground link for changed code

I imagine these were made and then this syntax change happened and it didn't get updated.

Changes invariant method to take &self instead of magic pre argument, and inductive proof stubs to take Self instead of the named type (it fails macro expansion with e.g. post: AdderMachine)

tjhance commented 4 days ago

thanks!