[Why3-club] why3ml output

Frédéric Besson frederic.besson at inria.fr
Mon Feb 6 10:34:01 CET 2012


As JC explained this WE (great lecture!), modules do not (yet) accommodate for cloning -- but theories do.
Thus, I am trying to run why3ml, generate the theory. Back in the theory world, I could clone again and so on.

Perhaps, I am doing something wrong, but the theory  generated by why3ml does not seem to compile with why3.
Is there an option to make it work ?
(At first view, imports are commented out and there are missing parentheses...)


More information about the Why3-club mailing list