From ee4cbbeb142d072c1d432ec2d167a6c430733f94 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Sat, 16 Aug 2025 11:19:07 +0200 Subject: [PATCH] fix: remove duplicate `mpure_intro` tactic definition (#9938) This PR removes a duplicate `mpure_intro` tactic definition. --- src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean index 04609a8cba..a7fc71284e 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean @@ -53,10 +53,8 @@ def elabMPure : Tactic replaceMainGoal [m.mvarId!] | _ => throwUnsupportedSyntax -macro "mpure_intro" : tactic => `(tactic| apply Pure.intro) - def MGoal.triviallyPure (goal : MGoal) : OptionT MetaM Expr := do let mv ← mkFreshExprMVar goal.toExpr - let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply Pure.intro; trivial)) catch _ => failure + let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); trivial)) catch _ => failure | failure return mv