[Why3-club] inlining functions or explicit predicates

Jean-Jacques Levy 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!

-JJ-

ps/ I’m using old release 0.88.3 :-(


More information about the Why3-club mailing list