New keywords in 4.11.0rc3

Stream: lean4

[Eric Wieser]

I note that 4.11.0rc3 introduces an omit keyword, that prevents any existing code from using omit as a local variable name.

Given that there is no context in which both are legal, should the parser be relaxed from "omit" to &"omit"? Or are there reasons this is a bad user experience / that this isn't technically possible?

[Kim Morrison]

I don't know about the technically possibility side, but I agree it would be better to allow it as a local variable name if possible. When updating mathlib there was one occurrence of this problem, in a tactic, and I changed the variable name from omit to toOmit.

Did you have other examples of this breaking something? Seems relatively minor if not.

[Eric Wieser]

Yes, it was that example that prompted this thread. I agree this is minor, but if the fix is really just a single character then it is probably worthwhile so as not to break downstream code.

[Sebastian Ullrich]

This is not an option for command keywords