Spurious "unused at/old" warning in lemma function parameters
Passing a lemma function parameter in the form (pure { x at L }) seems to trigger a spurious "unused at/old" warning.
In the example below, the at
operator at line 9 works as expected, but the following warning is emitted:
File "atold.mlw", line 9, characters 17-18:
warning: this `at'/`old' operator is never used
use int.Int
let lemma l (x:int) requires { x <> 0 } ensures { x * x > 0 } = ()
let f () =
let ref x = any int ensures { result <> 0 } in
label L in
x <- -3;
l (pure { x at L });
assert { (x at L) * (x at L) > 0 };