search

nomeata / loogle

Mathlib search tool
https://loogle.lean-lang.org/
Apache License 2.0
50 stars 6 forks source link

loogle easily confused by keywords like `repeat` #15

Open philderbeast opened 3 months ago

philderbeast commented 3 months ago

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 commented 3 months ago

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 commented 3 months ago

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.