Topic: jump to definition
Kevin Buzzard (Feb 21 2021 at 17:49):
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.
Last updated: May 07 2021 at 12:15 UTC