Definition
Elaboration (Lean)
Elaboration translates Lean source syntax into fully specified expressions for its kernel to check. It resolves names and notation, infers omitted types and implicit arguments, and invokes instance synthesis for instance arguments.
Information omitted from the source must be recovered from declarations and context; if it cannot be determined, elaboration reports an error. The kernel checks the resulting expression rather than trusting the elaborator’s choices.