until is a keyword?

Stream: lean4

[Colin Gordon]

I've just found an interesting quirk in Lean 4.0.0 m4:

inductive foo where
| unti

is totally fine, a boring type equivalent to unit. But if I complete "unti" to "until":

inductive foo where
| until

I get an error: "until" is underlined (VSCode Lean 4 mode) with the message "expected identifier". So I guess "until" is a reserved keyword? I can't find any docs on what it might be for; is it just reserved for future use?

Not a big deal (I just won't use 'until' as a constructor name), but it took me a minute to figure out why Lean wasn't happy with my inductive definition of LTL formulas, and now I'm curious about what the future (or current?) use case might be.

[Sébastien Michelland]

It's an extension of do notation which is part of the repeat ... until loop.

[Colin Gordon]

ah, of course! thanks

[Jannis Limperg]

Heh, I didn't know this existed. In general, you can use keywords as identifiers if you write «until».

[Jannis Limperg]

Btw m4 is very outdated; if you have problems with it, you may want to try a recent nightly. The nightlies tend to be reasonably stable as well.