Check notation

Stream: new members

[Kenny Lau]

How do I #check a notation? e.g. I want to see where < is defined using #check.

[Aaron Liu]

I think you can use #find for that

[Damiano Testa]

#find_syntax "<" suggests

In `Init.BinderPredicates`:
  Lean.«binderTerm<_»: '<'

[Kyle Miller]

I usually do #check 1 < 2 and "go to definition" on <

[Kyle Miller]

That's... an answer @Damiano Testa, but a very unexpected result.

[Damiano Testa]

Possibly, I was a bit surprised, but still found it potentially useful! :shrug:

[Damiano Testa]

(I am mostly still trying to see how #find_syntax performs "in the wild", so it was partially an internal test.)

[Kyle Miller]

I didn't mean to criticize #find_syntax, sorry if it came across that way. That answer isn't incorrect, but it's the < that's used for extended binders, which is interesting.

[Damiano Testa]

Yes, it is a "niche" answer. I'd like to see if it could also give a more "expected" answer.

[Damiano Testa]

My idea with #find_syntax was that it would be useful for situations where you would just copy-paste some notation, with no understanding of what was going on, and still receive a "good" answer. I know that this is not yet the case, so I'm experimenting more heuristics still.

[Damiano Testa]

Actually, I overlooked that it also suggested docs#«term_<_», which I consider a fair answer to the question of where < is defined! :slight_smile:

[Damiano Testa]

Maybe #find_syntax should "highlight" answers that are an exact match for the input surrounded by _.