structure-like custom syntax

Stream: lean4

[James Gallicchio]

I'm just starting to learn how the parsing infrastructure works (mainly via the metaprogramming tutorial book) -- is there a standard way to include the structure-like binder syntax in a syntax declaration?

Looking to parse commands of this form:

extensible Foo where
  bar : Baz

[James Gallicchio]

Also, is there somewhere in the compiler code base where the standard syntax is defined? (defs, structures, etc)

I'd find it helpful to learn from how the built-in syntax works

[Henrik Böving]

There is lots of locations where syntax is defined, notably:

• https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean
• https://github.com/leanprover/lean4/blob/master/src/Init/NotationExtra.lean

in Init and more spread throughout the compiler, notably here:

• https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Term.lean
• https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Command.lean

but also in a couple of other locations, the specific elaborator for structure is here: https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Structure.lean
and its syntax here: https://github.com/leanprover/lean4/blob/master/src/Lean/Parser/Command.lean#L112

[James Gallicchio]

Ah, thank you greatly

[pcpthm]

Also, syntax elements are linked (go to definition) in VSCode after import Lean.

import Lean
structure S where
  x : Nat

Then Ctrl+click on structure token will open this elaborator definition,

@[builtinCommandElab declaration]
def elabDeclaration : CommandElab := fun stx => do

and clicking declaration name in @[builtinCommandElab declaration] will open this parser definition.

[James Gallicchio]

Oh, this is very helpful to know :D