Hello Guillaume, Le 19/08/2016 à 18:02, Guillaume Melquiond a écrit : > 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
Oops, I was fooled by the error message (pointing on "match ((b1, b2))"). Now it works! For the record, here is the workaround: """ module Execute_test type bool_t = DTrue | DFalse (* work-around for execute bug in Why3 0.87.0 *) function bool_t_of_bool (b : bool) : bool_t = if b then DTrue else DFalse let f (cmd_previous cmd_current : bool) : bool = let b1, b2 = (bool_t_of_bool cmd_previous, bool_t_of_bool cmd_current) in match b1, b2 with | DFalse, DTrue -> True | _, _ -> False end let test () = f False True end """ Thanks! david _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
