Calling a variable "_" is not enough to override default "result" name
Hello,
The following is probably expected but I will raise the issue anyway. In the following program, calling the returned result _
is not enough to shadow the result
variable.
use int.Int
type t
let f (x: t) : (_: bool)
(* should not be possible to call result here ? *)
ensures { result = true }
=
true
let g (x: t) : (_t: bool)
ensures { _t (*result*) = true }
=
true
Is it possible to rename result in that case too ? I know that this would make the result value unusable but this is the user intended behavior in my opinion.