Patterns for local ghost values too restrictive
The parser seems to be too restrictive for patterns when defining local ghost values
by let ghost PATTERN = EXPR in EXPR
. Each of the lines marked with a-c are
refused with error "illegal ghost qualifier":
let constant u : unit =
let e = (0, 0) in
let ghost _ = e in (* a *)
let ghost _, y = e in (* b *)
let ghost (x, y) = e in (* c *)
()
But the lines marked with e-g are accepted.
let constant u : unit =
let e = (0, 0) in
let ghost _x = e in (* e *)
let ghost _x, y = e in (* f *)
let ghost x, y = e in (* g *)
()
I would expect all lines a-g syntactically valid in Why3 (as they were in version 0.88).