inductive Lean.Meta.Sym.IntrosResult : Type

• failed : IntrosResult
• goal (newDecls : Array FVarId) (mvarId : MVarId) : IntrosResult

def Lean.Meta.Sym.intros (mvarId : MVarId) (names : Array Name := #[]) : SymM IntrosResult

Introduces leading binders (universal quantifiers and let-expressions) from the goal's target type.

If names is non-empty, introduces (at most) names.size binders using the provided names. If names is empty, introduces all leading binders using inaccessible names.

Returns .goal newDecls mvarId with new introduced free variable Ids and the updated goal. Returns .failed if no new declaration was introduced.

Equations

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

def Lean.Meta.Sym.introN (mvarId : MVarId) (num : Nat) : SymM IntrosResult

Introduces exactly num binders from the goal's target type.

Returns .goal newDecls mvarId if successful where newDecls are the introduced free variable IDs, mvarId the updated goal. Returns .failed if it was not possible to introduce num new local declarations.

Equations

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