jump to definition

Stream: lean4

[Kevin Buzzard]

I want to define notation ∈. I don't know how to find out if this is defined already in Lean 4 -- #print notation + doesn't work and + is certainly defined . My instinct is to look at how other notation is defined but I don't know how to jump to definition.

#check Add.add 5
#check 5 +

both work, but I can't right click on them. I literally have no idea where the core Lean files are on my system (Ubuntu 18.04, stable installed via elan, no nix). Maybe I'll just browse the Lean 4 repo on github but it would be good if I knew how to verify if ∈ was defined -- I assume it's not, but #check 5 ∈ just gives me two "expected term" errors and I don't know what this means.