debug symbols

Stream: general

[Björn Fischer]

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]

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]

Also in VScode: Ctrl-click on a symbol. and #print some_name will print the full term definition (can be ugly). Finally Ctrl-T will allow you to search (with completion) for names in the library.

[Björn Fischer]

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 #nat.add.

[Rob Lewis]

There's environment.decl_olean and environment.decl_pos.

[Björn Fischer]

@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 --quiet.

[Floris van Doorn]

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.