The Lean.Parser.Command.elab_rules : command
elab_rules
command takes a sequence of elaboration rules, specified as syntax pattern matches, and adds each as an elaborator.
The rules are attempted in order, before previously-defined elaborators, and later elaborators may add further options.
command ::= ... |docComment? (@[attrInstance,*])?
A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure. At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use `plainDocComment` to always treat the contents as plain text. A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/` in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
attrKind elab_rules ((kind := ident))? (: ident)? (<= ident)? (|
`attrKind` matches `("scoped" <|> "local")?`, used before an attribute like `@[local simp]`.
`((
Syntax quotation for terms.
p:ident|)?Suitable syntax for
p : ident
p ) => term)*
p : ident