Declaration Name Elaborator

Provides the decl_name% term elaborator, which resolves an identifier to its fully qualified Lean.Name at compile time. This ensures that references to declarations are checked by the compiler and will cause build failures if the target declaration is renamed or removed.

def «termDecl_name%_» : Lean.ParserDescr

decl_name% Foo.bar resolves the identifier to verify the declaration exists, then returns the corresponding Lean.Name. Build fails if the declaration is renamed or removed.

Equations

• «termDecl_name%_» = Lean.ParserDescr.node `«termDecl_name%_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "decl_name% ") (Lean.ParserDescr.const `ident))