loogle easily confused by keywords like repeat

[philderbeast]

I was looking for something like repeat on hoogle. The search for repeat on loogle comes back with;

<input>:1:0: expected end of input

Other searches come back fine, like the search for sin that comes back with unknown identifier 'sin' and then a list of possibilities.

[nomeata]

That’s because repeat is a keyword in Lean. If you want to search for definitions lemmas having repeat in the name, use "repeat".

Possibly loogle could, if there is a parse error, check if the input was just a single word and be more helpful then.

[philderbeast]

I was wondering about keywords because I got the same error when I searched for def on loogle but didn't want to jump the gun on probable cause.