Documentation

Lean.Elab.Quotation.Precheck

Equations
  • Lean.Elab.Term.Quotation.mkPrecheckAttribute = Lean.KeyedDeclsAttribute.init { builtinName := `builtinQuotPrecheck, name := `quotPrecheck, descr := "Register a double backtick syntax quotation pre-check.\n\n[quotPrecheck k] registers a declaration of type `Lean.Elab.Term.Quotation.Precheck` for the `SyntaxNodeKind` `k`.\nIt should implement eager name analysis on the passed syntax by throwing an exception on unbound identifiers,\nand calling `precheck` recursively on nested terms, potentially with an extended local context (`withNewLocal`).\nMacros without registered precheck hook are unfolded, and identifier-less syntax is ultimately assumed to be well-formed.", valueTypeName := `Lean.Elab.Term.Quotation.Precheck, evalKey := fun builtin stx => Lean.Attribute.Builtin.getId stx, onAdded := fun builtin declName => pure () } `Lean.Elab.Term.Quotation.precheckAttribute
Equations
Equations
Equations