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... julia > > Best regards, > -- > Jean-Christophe > > 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@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
