Questions tagged [why3ml]

I want to verify a function with a lambda. For instance: let map (t : array int) (f : array int -> array int) : array int = f t However, this yields an error: File "map_reduce.mlw", line 25, characters 4-7: This application instantiates…

With the latest version of Why3 (1.0.0), when I attempt to do something like the following: let add_one (n: int) : int = n+1 predicate is_successor_of (n: int) (m: int) = m = add_one n I get an error of the form: File "../something.why", line x,…

In other ML-variants (such as SML) it is possible to do something like this: case l of (true, _) => false | (false,true) => false | (false,false) => true However, doing a similar thing using the Why3ML match declaration raises a syntax…