Why3 should not introduce spaces in identifiers
Spaces are introduced in identifiers in some cases. This makes it impossible for the user to use these identifiers in arguments of transformations.
An example with records is the following:
use int.Int
type r = {a : int; b : int}
let f (x y: r): bool
ensures {x.a = y.a}
=
true
To explicitly show the problem use the following transformations:
introduce_premises
destruct_term x
assert (x2 = mk r x1 x)
@marche suggest to use tick '
instead of space because the user would still not be able to define those in .mlw file but they would be able to use them. Here, the result would be something along the lines of r'mk
.
Note that spaces also appear in the names of goals: they could be removed in favor of '
too. For example: f'VC
.
On this issue, I will try to make a MR with the simple replacement of mk
with 'mk
to see if it could work. Note that I also expect to change accordingly any code that would recognize a record by looking if its name begins with mk
.