why3
| Crates.io | why3 |
| lib.rs | why3 |
| version | |
| source | src |
| created_at | 2024-07-30 19:20:17.72335+00 |
| updated_at | 2025-03-03 12:10:56.94018+00 |
| description | Why3 AST and pretty printers |
| homepage | |
| repository | https://github.com/creusot-rs/creusot |
| max_upload_size | |
| id | 1320256 |
| Cargo.toml error: | TOML parse error at line 18, column 1 | 18 | autolib = false | ^^^^^^^ unknown field `autolib`, expected one of `name`, `version`, `edition`, `authors`, `description`, `readme`, `license`, `repository`, `homepage`, `documentation`, `build`, `resolver`, `links`, `default-run`, `default_dash_run`, `rust-version`, `rust_dash_version`, `rust_version`, `license-file`, `license_dash_file`, `license_file`, `licenseFile`, `license_capital_file`, `forced-target`, `forced_dash_target`, `autobins`, `autotests`, `autoexamples`, `autobenches`, `publish`, `metadata`, `keywords`, `categories`, `exclude`, `include` |
| size | 0 |
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.