On 19/08/2016 11:20, David MENTRE wrote: > Hello, > > When trying to execute the attached WhyML file, I get following error: > """ > $ why3 -C why3.config execute execute_test.mlw Execute_test.test > Execution of Execute_test.test (): > type: bool > > > Execution error: Cannot execute expression > match ((cmd_previous, > cmd_current)) with > | False, True -> (True) > | _, _ -> (False) > end > """ > > Is this a bug?
Yes. Boolean are hardcoded in the interpreter, but somehow the match construct does not know about them. > Should I open a bug on Why3 issue tracker? Don't bother, it should be easy enough to fix (assuming my interpretation is correct). > Is there a work-around? In the meantime, using your own boolean type rather than the standard one should do the trick. Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
