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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.addBuiltinIncrementalElab decl = ST.Ref.modify Lean.Elab.builtinIncrementalElabs fun (s : Lean.NameSet) => s.insert decl

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].

Equations

• One or more equations did not get rendered due to their size.