def Lean.Elab.Term.expandDeclId (currNamespace : Name) (currLevelNames : List Name) (declId : Syntax) (modifiers : Modifiers) : TermElabM ExpandDeclIdResult

opaque Lean.Elab.incrementalAttr : TagAttribute

Marks an elaborator (tactic or command, currently) as supporting incremental elaboration.

For unmarked elaborators, the corresponding snapshot bundle field in the elaboration context is unset so as to prevent accidental, incorrect reuse.

opaque Lean.Elab.builtinIncrementalElabs : IO.Ref NameSet

def Lean.Elab.addBuiltinIncrementalElab (decl : Name) : IO Unit

def Lean.Elab.isIncrementalElab {m : Type → Type} [Monad m] [MonadEnv m] [MonadLiftT IO m] (decl : Name) : m Bool

Checks whether a declaration is annotated with [builtin_incremental] or [incremental].