[Why3-club] always inline a predicate
julia.lawall at lip6.fr
Thu Mar 7 20:15:58 CET 2019
On Thu, 7 Mar 2019, Jean-Christophe Filliatre wrote:
> Dear Julia,
> There is a meta "inline:no" which can be used to indicate that a
> function/predicate *must not* be inlined (by inline_all or inline_goal).
> Use it like this
> meta "inline:no" predicate foo
> Unless I'm mistaken, there is no way to indicate the opposite i.e. that
> a symbol must always be inlined.
OK, I've been sprinkling
meta "rewrite_def" proposition foo
But I'm not sure if it really has an impact...
> Best regards,
> On 3/3/19 8:18 AM, Julia Lawall wrote:
> > Hello,
> > Is there an annotation that can be put in a .mlw to cause a predicate
> > always to be inlined? Currently, I have to guess when inline_goal or
> > inline_all would be useful, and neither is really satisfactory, because I
> > don't want to inline everything, but just this one predicate.
> > thanks,
> > julia
> > _______________________________________________
> > Why3-club mailing list
> > Why3-club at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club