Topic: debug symbols
Björn Fischer (Jul 29 2019 at 16:23):
Given some name, can I (if applicable) find its definition location (lean file and line(s)) using a tactic or by some other means?
Jeremy Avigad (Jul 29 2019 at 16:28):
In VSCode, I usually type e.g.
#check nat.add, then right-click on
nat.add and choose "Go to Definition". Similar things work for notation.
Johan Commelin (Jul 29 2019 at 16:38):
Also in VScode:
Ctrl-click on a symbol. and
#print some_name will print the full term definition (can be ugly). Finally
T will allow you to search (with completion) for names in the library.
Björn Fischer (Jul 29 2019 at 16:38):
Thanks @Jeremy Avigad I need this for automation, though. I want to import definitions (by their name) into Latex listings without having to copy/paste.
FYI: In VSCode you can also lookup definitions by typing Ctrl+P and then
Rob Lewis (Jul 29 2019 at 17:12):
Björn Fischer (Jul 30 2019 at 11:20):
@Rob Lewis Thanks! Exactly what I'm looking for.
Follow up question: I've noticed that Lean (surprisingly) prints warnings to stdout. Can this be disabled or changed to stderr? I've tried
Floris van Doorn (Jul 30 2019 at 13:58):
FYI: In VSCode you can also lookup definitions by typing Ctrl+P and then #nat.add.
Nice! I didn't know this. That sounds incredibly useful if you're in a file which you don't want to modify.
Last updated: May 08 2021 at 10:12 UTC