[Why3-club] WhyML questions: function without body? polymorphic Sum?
dmentre at linux-france.org
Tue Nov 27 17:54:07 CET 2012
2012/11/27 Guillaume Melquiond <guillaume.melquiond at inria.fr>:
>> 1. Is it possible to specify behaviour of "get_cont_value" without
>> giving its body (i.e. only ensures, requires, ...)? I am currently at
>> the specification phase and I am not interested in function bodies
>> (and their correctness).
> Sure, just stops before "=" and change "let" into "val".
More information about the Why3-club