[Why3-club] inlining functions or explicit predicates
Claude.Marche at inria.fr
Fri Feb 15 17:08:33 CET 2019
As you remark, Why3 0.88 is now quite outdated and my answer may not be
very accurate. As far as I remember, the former "Inline" button was
applying the transformation "inline_goal" which has the effect of
inlining the defined function symbols appearing in an outermost position
in the goal.
The doc for the transformations are obtained when typing `why3
--list-transforms', and some of them are documented in a bit more
details in the manual : "inline_*" are documented at the beginning of
In Why3 1.x, the user interface for applying transformations is much
more powerful, in your case you would probably want to type "unfold foo"
where "foo" is your function symbol. The documentation is also visible
I don't know how to help more without seeing the exact example you have.
Le 14/02/2019 à 16:20, Jean-Jacques Levy a écrit :
> Dear Why3 Friends,
> is there any doc about the functionality of the "Inline" button in the Why3 IDE ?
> Same for inline_all, inline_goal, inline_trivial..
> My current problem is that the inlined version of a trivial function works with automatic provers, but I cannot find a way of forcing that inlining.
> Many many thanks for you help!
> ps/ I’m using old release 0.88.3 :-(
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club