← Mathematical handbook

def Lean.Elab.Tactic.evalExposeNames : Tactic

Equations

• Lean.Elab.Tactic.evalExposeNames x✝ = Lean.Elab.Tactic.liftMetaTactic1 fun (mvarId : Lean.MVarId) => do let a ← mvarId.exposeNames pure (some a)