max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: remove duplicate mpure_intro tactic definition (#9938)

Browse source 
This PR removes a duplicate `mpure_intro` tactic definition.
This commit is contained in:
Sebastian Graf 2025-08-16 11:19:07 +02:00 • committed by GitHub
parent 0e968f010a
commit ee4cbbeb14
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean
View file

@ -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