Zulip Chat Archive

Stream: lean4

Topic: jump to definition

view this post on Zulip 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