feat: proper syntax for configuring simp

src/Init/Notation.lean

@@ -265,7 +265,7 @@ syntax simpPre   := "↓"
 syntax simpPost  := "↑"
 syntax simpLemma := (simpPre <|> simpPost)? term
 syntax simpErase := "-" ident
-syntax (name := simp) "simp " (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (colGt term)? (location)? : tactic
+syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic
 
 -- Auxiliary macro for lifting have/suffices/let/...
 -- It makes sure the "continuation" `?_` is the main goal after refining

src/Lean/Elab/Tactic/Simp.lean

@@ -76,7 +76,7 @@ def elabSimpConfig (optConfig : Syntax) : TermElabM Meta.Simp.Config := do
     return {}
   else
     withLCtx {} {} <| withNewMCtxDepth <| Term.withSynthesize do
-      let c ← Term.elabTermEnsuringType optConfig[0][3] (Lean.mkConst ``Meta.Simp.Config)
+      let c ← Term.elabTermEnsuringType optConfig[3] (Lean.mkConst ``Meta.Simp.Config)
       evalSimpConfig (← instantiateMVars c)
 
 /-- Elaborate extra simp lemmas provided to `simp`. `stx` is of the `simpLemma,*` -/

tests/lean/run/ifcongr.lean

@@ -7,7 +7,7 @@ theorem ex1 (x : Nat) : (if x > 3 ∧ True then 1 else 2) = (if x > 3 then 1 els
  by simp
 
 theorem ex2 (x : Nat) : (if x = 0 ∧ True then x + 1 else 2 + x) = (if x = 0 then 1 else x + 2) :=
-  by simp {contextual := true}
+  by simp (config := {contextual := true})
 
 #print ex2
 

tests/lean/run/simp4.lean

@@ -37,7 +37,7 @@ theorem ex6
   (f : Nat → Nat)
   (x y : Nat)
   : (fun (h : y = 0) => y + x) = (fun _ => x + 0) := by
- simp { contextual := true }
+ simp (config := { contextual := true })
 
 theorem ex7 (x : Nat) : (let y := x + 0; y + y) = x + x := by
   simp
@@ -46,7 +46,7 @@ theorem ex7 (x : Nat) : (let y := x + 0; y + y) = x + x := by
   propext <| Iff.intro (fun _ => trivial) (fun _ _ => trivial)
 
 theorem ex8 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
-  simp { contextual := true }
+  simp (config := { contextual := true })
 
 theorem ex9 (y x : Nat) : y = 0 → x + y = 0 → x = 0 := by
   simp

tests/lean/run/simp6.lean

@@ -21,7 +21,7 @@ theorem ex6 : (if "hello" = "world" then 1 else 2) = 2 :=
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
-  simp { decide := false }
+  simp (config := { decide := false })
   simp
 
 theorem ex8 : (10 + 2000 = 20) = False :=

tests/lean/simpcfg.lean

@@ -1,5 +1,5 @@
 theorem ex6 (f : Nat → Nat) (x y z : Nat) (h : (x, z).1 = (fun x => x) y) : f x = f y := by
-  simp { beta := false } at h
+  simp (config := { beta := false }) at h
   traceState
   simp at h
   traceState