Warn about spurious `rec` keyword
Unlike OCaml, Why3 does not warn about useless rec
keyword, could it do it? It would avoid strange behaviours like in
let rec f (x:int) ensures { result > x } = x+1
let rec ghost g (x:int) ensures { result > x } = x+1
let rec ghost h (x:int) variant { 0 } ensures { result > x } = x+1
for f
, there is no warning, for g
there is an error This ghost function may not terminate
, but it is OK for h
of course.