Is `until` reserved?

Stream: lean4

[Mrigank Pawagi]

until seems to be some sort of a reserved word in lean 4, but I am unable to find it in the documentation. I am just curious because I did something like the following

def until := 1

but got unexpected token 'until'; expected identifier.

[Aaron Liu]

docs#Lean.doElemRepeat__Until_

[Mrigank Pawagi]

Thanks! This line in the code makes it clear:

syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem

I have used repeat but not repeat ... until.

[Damiano Testa]

In case it is helpful for some other time, you could also have found out about this as follows:

import Mathlib.Tactic.FindSyntax

/--
info: Found 1 use among 579 syntax declarations
In `Init.While`:
  Lean.doElemRepeat__Until_: 'repeat  _ until'
-/
#guard_msgs in
#find_syntax "until"

[Aaron Liu]

I just did a @loogle "until"

[loogle]

:search: String.nextUntil, Lean.doElemRepeat__Until_, and 65 more

[Mrigank Pawagi]

Thanks so much for the tips, @Damiano Testa and @Aaron Liu. I am new to Lean and this seems very useful!