Dear Why3 Friends,
is there any doc about the functionality of the "Inline" button in the Why3
IDE ?
Same for inline_all, inline_goal, inline_trivial..
My current problem is that the inlined version of a trivial function works with
automatic provers, but I cannot find a way of forcing that
(ERRATUM: Date changed!)
* Frama-C & SPARK Day 2019 *
Date: Monday, June 3, 2019
Location: Paris, La Fabrique Événementielle (52 ter rue des Vinaigriers,
75010 Paris)
This one-day workshop aims at gathering both academic and industrial
users of the environments Frama-C and SPARK, for
