[Why3-club] always inline a predicate

Guillaume Melquiond guillaume.melquiond at inria.fr
Fri Mar 8 11:05:54 CET 2019


Le 07/03/2019 à 20:15, Julia Lawall a écrit :

> OK, I've been sprinkling
> 
> meta "rewrite_def" proposition foo
> 
> But I'm not sure if it really has an impact...

This meta is mostly meant for the "compute_specified" transformation. If 
you manually apply this transformation, all the tagged definitions 
should be unfolded.

Best regards,

Guillaume


More information about the Why3-club mailing list