GitLab

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 .