Dear JJ,
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 http://why3.lri.fr/doc/technical.html#sec128
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 interactively.
I don't know how to help more without seeing the exact example you have. - Claude 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! -JJ- ps/ I’m using old release 0.88.3 :-( _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
