search

formal-land / coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
GNU Affero General Public License v3.0
418 stars 14 forks source link

Add an example of test in Coq for the type-checker #611

Closed clarus closed 3 weeks ago

clarus commented 1 month ago

In addition to adding an example of simulation for one of the tests, this pull request removes the string parameter from the error monad to represent panics.

This should simplify the use of this monad a bit, and it allows to make a panic with a richer payload than a string for debugging purposes.