Syntax `(fun x -> ...)` should always denote a lambda-expression, not a program
It seems that in the current Why3, the syntax (fun x -> e)
is interpreted either as a logic function or as a program function, depending on the context. For example in
let test () =
let ref f = (fun x -> x+1) in
assert { f 0 = 1 };
let g = (fun x -> x+1) in
assert { g 1 = 2 }
the first function f
is a logic function, and as such the first assert is OK, whereas the second function g
is a program function, and the second assert triggers the error unbound symbol g
. My arguments against considering g
as a program function :
- This is error-prone
- The error message above is incomprehensible
- I feel there is no case where one would like to define an anonymous program function since Why3 does not support higher-order programs.