Skip to content

[ppx] why3 extension for extracted code

Loïc Correnson requested to merge feature/ppx into master

Introduces a PPX rewriter to call Why-3 extracted code from OCaml.

⚠ this PPX extension only works with an experimental branch of why3 that generates symbol maps.

Edited by Loïc Correnson

Merge request reports