Ambiguous `result` notation
Hello,
It's possible to use the name result
for ident defined inside functions. I thought this was a keyword (or disallowed somehow). So, it is possible for the user to create a variable that cannot be used in the postcondition like in the following provable example:
let example (result : int) =
requires { result = 3 }
ensures { result = 4 }
result + 1
I don't think any direct user of the tool would try to create a result
ident but it may be a problem for users who generate their .mlw file (or users of the API).
Also, is it possible that other constants are introduced and may cause problems too ?