From 205b42a397bf80bbfad5632ea7749f9b6e6ccbdc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 17 Mar 2021 16:37:04 -0700
Subject: [PATCH] feat: proper syntax for configuring `simp`

---
 src/Init/Notation.lean         | 2 +-
 src/Lean/Elab/Tactic/Simp.lean | 2 +-
 tests/lean/run/ifcongr.lean    | 2 +-
 tests/lean/run/simp4.lean      | 4 ++--
 tests/lean/run/simp6.lean      | 2 +-
 tests/lean/simpcfg.lean        | 2 +-
 6 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 167dc46934..533e663811 100644
--- a/src/Init/Notation.lean
+++ b/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
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index a8247154ca..7896625f0c 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/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,*` -/
diff --git a/tests/lean/run/ifcongr.lean b/tests/lean/run/ifcongr.lean
index e76e45e7dd..06d4ac52d2 100644
--- a/tests/lean/run/ifcongr.lean
+++ b/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
 
diff --git a/tests/lean/run/simp4.lean b/tests/lean/run/simp4.lean
index 9046587cbe..30352a58b4 100644
--- a/tests/lean/run/simp4.lean
+++ b/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
diff --git a/tests/lean/run/simp6.lean b/tests/lean/run/simp6.lean
index ad1064a690..a35d361c95 100644
--- a/tests/lean/run/simp6.lean
+++ b/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 :=
diff --git a/tests/lean/simpcfg.lean b/tests/lean/simpcfg.lean
index 7d21c2c7e3..e0803ad9ed 100644
--- a/tests/lean/simpcfg.lean
+++ b/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