where are parsers/grammar for def, inductive, etc defined?

Stream: new members

[Mark Aagaard]

I'm trying to understand the grammar and the various parsers that are used by def and inductive. Is there source code where the parsers for these commands are defined?

-mark

[Vlad Tsyrklevich]

I believe you're looking for https://github.com/leanprover/lean4/blob/93d4ae6635c0c755c9f7368f9b99483d4557b7a6/src/Lean/Parser/Command.lean#L140

[Kyle Miller]

If you have the Lean package imported, then in VS Code you can right click on, for example, def, and then "Go to declaration" to get to the syntax declaration.

[Mark Aagaard]

Vlad and Kyle: Thanks!
-mark