[Why3-club] always inline a predicate

Julia Lawall julia.lawall at lip6.fr
Sun Mar 3 08:18:01 CET 2019


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


More information about the Why3-club mailing list