Tactic combinators in TacticM.

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

Analogue of liftMetaTactic for tactics that do not return any goals.

Equations

• Lean.Elab.Tactic.liftMetaFinishingTactic tac = Lean.Elab.Tactic.liftMetaTactic fun (g : Lean.MVarId) => do tac g pure []