feat: simp only

src/Init/Notation.lean

@@ -256,7 +256,7 @@ syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)
 syntax simpPre := "↓"
 syntax simpPost := "↑"
 syntax simpLemma := (simpPre <|> simpPost)? term
-syntax (name := simp) "simp " ("[" simpLemma,* "]")? (colGt term)? (location)? : tactic
+syntax (name := simp) "simp " (&"only ")? ("[" simpLemma,* "]")? (colGt term)? (location)? : tactic
 
 syntax (name := «have») "have " haveDecl : tactic
 syntax (name := «suffices») "suffices " sufficesDecl : tactic

src/Lean/Elab/Tactic/Simp.lean

@@ -119,10 +119,15 @@ where
       return none
 
 /-
-  "simp " ("[" simpLemma,* "]")? (colGt term)? (location)?
+  "simp " ("only ")? ("[" simpLemma,* "]")? (colGt term)? (location)?
 -/
 @[builtinTactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do
-  let ctx ← elabSimpLemmas stx[2] { config := (← elabSimpConfig stx[3]), simpLemmas := (← getSimpLemmas), congrLemmas := (← getCongrLemmas) }
+  let simpOnly := !stx[1].isNone
+  let ctx  ← elabSimpLemmas stx[2] {
+    config      := (← elabSimpConfig stx[3])
+    simpLemmas  := if simpOnly then {} else (← getSimpLemmas)
+    congrLemmas := (← getCongrLemmas)
+  }
   let loc := expandOptLocation stx[4]
   match loc with
   | Location.target => simpTarget ctx

tests/lean/run/simpOnly.lean

@@ -0,0 +1,13 @@
+theorem ex1 (n m : Nat) : 0 + (n, m).1 = n := by
+  simp only
+  rw [Nat.zero_add]
+
+theorem ex2 (n m : Nat) : 0 + (n, m).1 = n := by
+  simp
+
+theorem ex3 (n m : Nat) : 0 + (n, m).1 + 0 = n := by
+  simp only [Nat.add_zero]
+  rw [Nat.zero_add]
+
+theorem ex4 (n m : Nat) : 0 + (n, m).1 + 0 = n := by
+  simp