On 10/09/2016 22:58, Per Lindgren wrote:
> Hi Folks.
>
> I’ve observed an obstacle to the code extraction of “let” functions with
> ghost parameters. In cases the generated function code drops ghost
> parameters, while the corresponding calls, do not (leading to compilation
> error later on the
Hi Folks.
I’ve observed an obstacle to the code extraction of “let” functions with ghost
parameters. In cases the generated function code drops ghost parameters, while
the corresponding calls, do not (leading to compilation error later on the
OCaml side).
I’m no expert at the Why3 internals, b
