verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.06k stars 58 forks source link

Documentation for arithmetic and mixed triggers #1192

Open matthias-brun opened 1 week ago

matthias-brun commented 1 week ago

I marked this as draft because I still need to extract the examples into example/test files but I'm waiting for @utaal's changes to the test harness to support multiple expecting-to-fail tests in a single file.

@Chris-Hawblitzel Feel free to adjust the text (or let me know what you'd like changed) if you think my text doesn't sufficiently dissuade people from using arithmetic/mixed triggers.

@jopolzin Please also have a read through and let me know if this is understandable.