Additional utilities in Lean.MVarId

def Lean.MVarId.let (g : MVarId) (h : Name) (v : Expr) (t : Option Expr := none) : MetaM (FVarId × MVarId)

Add the hypothesis h : t, given v : t, and return the new FVarId.

def Lean.MVarId.existsi (mvar : MVarId) (es : List Expr) : MetaM MVarId

Has the effect of refine ⟨e₁,e₂,⋯, ?_⟩.

def Lean.MVarId.intros! (mvarId : MVarId) : MetaM (Array FVarId × MVarId)

Applies intro repeatedly until it fails. We use this instead of Lean.MVarId.intros to allowing unfolding. For example, if we want to do introductions for propositions like ¬p, the ¬ needs to be unfolded into → False, and intros does not do such unfolding.

partial def Lean.MVarId.intros!.run (mvarId : MVarId) (acc : Array FVarId) (g : MVarId) : MetaM (Array FVarId × MVarId)

Implementation of intros!.

def Lean.MVarId.getType'' (mvarId : MVarId) : MetaM Expr

Get the type the given metavariable after instantiating metavariables and cleaning up annotations.

def Lean.Elab.Tactic.liftMetaTactic' (tac : MVarId → MetaM MVarId) : TacticM Unit

Analogue of liftMetaTactic for tactics that return a single goal.

def Lean.Elab.Tactic.run_for {α : Type} (mvarId : MVarId) (x : TacticM α) : TermElabM (Option α × List MVarId)

Copy of Lean.Elab.Tactic.run that can return a value.