[Why3-club] why3 execute: Cannot execute expression match
guillaume.melquiond at inria.fr
Fri Aug 19 18:02:41 CEST 2016
On 19/08/2016 17:45, David MENTRE wrote:
>>>> Is there a work-around?
>> In the meantime, using your own boolean type rather than the standard
>> one should do the trick.
> I failed to do it despite several attempts, see attached execute_test.mlw:
You just moved the matching issue from f to bool_t_of_bool. You should
have written the latter function as
function bool_t_of_bool (b : bool) : bool_t
= if b then DTrue else DFalse
so that it doesn't match on boolean values.
More information about the Why3-club