[Why3-club] record simplifications

Johannes Kanig kanig at adacore.com
Fri Nov 16 18:27:16 CET 2012


On 11/16/2012 06:19 PM, Guillaume Melquiond wrote:
> If I am not mistaken, that is precisely what src/transform/eval_match.ml
> does. Except that it is only called by the WP, which would explain why
> it fails for you. (But I am no expert.)

Ah, I remember eval_match now, thanks. Is there a reason why that's not
exported as a regular transformation? Hardwiring it in the code would
make it unflexible wrt. ordering of transformations - consider the
inlining of "f" in the example.

-- 
Johannes Kanig <kanig at adacore.com>



More information about the Why3-club mailing list