[Why3-club] inlining functions or explicit predicates
jean-jacques.levy at inria.fr
Thu Feb 14 16:20:53 CET 2019
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 inlining.
Many many thanks for you help!
ps/ I’m using old release 0.88.3 :-(
More information about the Why3-club