Documentation

Mathlib.Lean.Elab.Tactic.Meta

Additions to Lean.Elab.Tactic.Meta #

source
def Lean.Elab.runTactic' (mvarId : MVarId) (tacticCode : Syntax) (ctx : Term.Context := { }) (s : Term.State := { }) :
MetaM (List MVarId)

Apply the given tactic code to mvarId in MetaM.

This is a variant of Lean.Elab.runTactic that forgets the final Term.State.

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