Dear Claude, thanks for your answer. So I upgraded (with opam) why3 to release 1.1.1. (couldn’t find opam upgrade to 1.2.0!)
Now I’m facing a new problem with strange ‘ghost’ error. ----------------- module AAA use list.List use map.Map let rec set_1000 (s : list 'a)(f : map 'a int) = match s with | Nil -> f | Cons x s' -> (set_1000 s' f)[x <- 1000] end end ----------------- why3 execute aaa.mlw File "aaa.mlw", line 6, characters 8-16: Function set_1000 must be explicitly marked ghost ----------------- So why that message + where to insert the ghost keyword (couldn’t find!) ?? Cheers, -JJ- > Le 15 févr. 2019 à 17:08, Claude Marche <claude.mar...@inria.fr> a écrit : > > > 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
_______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
