[Why3-club] always inline a predicate

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Thu Mar 7 17:11:52 CET 2019

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.

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

More information about the Why3-club mailing list