Error when using a custom order in variant clause
use int.Int
predicate my_order (x y : int) =
x < y /\ x >= 0
let rec f () =
let ref x = 10 in
while x > 0 do
variant { [@variant:x] x with my_order }
x <- x - 1
done
With why3 prove variant.mlw
I get the error:
File "variant.mlw", line 6, character 0 to line 11, character 6:
Ident (->) is not yet declared
This comes from one of the MRs (probably !736 (merged) but I didn't test) that changed how VCs for variant are generated.