[Why3-club] WhyML questions: function without body? polymorphic Sum?

David MENTRE 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".

Thanks Guillaume!

d.



More information about the Why3-club mailing list