why3
| Crates.io | why3 |
| lib.rs | why3 |
| version | 0.5.0 |
| created_at | 2024-07-30 19:20:17.72335+00 |
| updated_at | 2025-04-23 13:55:55.845446+00 |
| description | Why3 AST and pretty printers |
| homepage | |
| repository | https://github.com/creusot-rs/creusot |
| max_upload_size | |
| id | 1320256 |
| size | 147,289 |
Xia Li-yao (Lysxia)
documentation
README
Why3
A Rust library furnishing the Why3 AST used by the Creusot verifier, and its associated pretty printer.
The library supports two input formats to why3: WhyML (.mlw), Coma (.coma).
As it stands the core Why3 Exp type is heavily burdened with tech debt associated to its evolution as an offsprout of creusot.
I hope to clean this up incrementally, but if you are planning on using why3 in a project, please contact me so I can reprioritize.