FormalConjecturesUtil/DeclName.lean

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.