1 unstable release
0.2.0 | Jul 30, 2024 |
---|
#203 in Value formatting
120KB
3.5K
SLoC
Why3
A Rust library furnishing the Why3 AST used by the Creusot verifier, and its associated pretty printer.
The library supports three input formats to why3: WhyML (.mlw
), coma (.coma
) and 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.
Dependencies
~4MB
~67K SLoC