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. Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
