1 unstable release

0.2.0 Jul 30, 2024

#203 in Value formatting

LGPL-2.1-or-later

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