fix: rw final goal state

src/Init/Data/Option/Basic.lean

@@ -14,10 +14,6 @@ def toMonad [Monad m] [Alternative m] : Option α → m α
   | none     => failure
   | some a   => pure a
 
-@[macroInline] def getD : Option α → α → α
-  | some x, _ => x
-  | none,   e => e
-
 @[inline] def toBool : Option α → Bool
   | some _ => true
   | none   => false

src/Init/Meta.lean

@@ -260,9 +260,6 @@ end Syntax
   | none => x
   | some ref => withRef ref x
 
-def mkAtom (val : String) : Syntax :=
-  Syntax.atom SourceInfo.none val
-
 @[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
   Syntax.node k args
 

src/Init/Notation.lean

@@ -252,21 +252,20 @@ syntax (name := erewriteSeq) "erewrite " rwRuleSeq (location)? : tactic
 syntax (name := rwSeq) "rw " rwRuleSeq (location)? : tactic
 syntax (name := erwSeq) "erw " rwRuleSeq (location)? : tactic
 
-private def withCheapRefl (tac : Syntax) : MacroM Syntax :=
-  `(tactic| $tac; try (withReducible rfl))
+def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Syntax := do
+  -- We show the `rfl` state on `]`
+  let seq   := stx[1]
+  let rbrak := seq[2]
+  -- Replace `]` token with one without position information in the expanded tactic
+  let seq   := seq.setArg 2 (mkAtom "]")
+  let tac   := stx.setKind kind |>.setArg 0 (mkAtomFrom stx atom) |>.setArg 1 seq
+  `(tactic| $tac; try (withReducible rfl%$rbrak))
 
-@[macro rwSeq]
-def expandRwSeq : Macro := fun stx =>
-  let rbrak := stx[1][2]
-  -- show "cheap refl" state on `]`
-  withRef rbrak <|
-    withCheapRefl (stx.setKind `Lean.Parser.Tactic.rewriteSeq |>.setArg 0 (mkAtomFrom stx "rewrite"))
+@[macro rwSeq] def expandRwSeq : Macro :=
+  rwWithRfl ``Lean.Parser.Tactic.rewriteSeq "rewrite"
 
-@[macro erwSeq]
-def expandERwSeq : Macro := fun stx =>
-  let rbrak := stx[1][2]
-  withRef rbrak <|
-    withCheapRefl (stx.setKind `Lean.Parser.Tactic.erewriteSeq |>.setArg 0 (mkAtomFrom stx "erewrite"))
+@[macro erwSeq] def expandERwSeq : Macro :=
+  rwWithRfl ``Lean.Parser.Tactic.erewriteSeq "erewrite"
 
 syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
 

src/Init/Prelude.lean

@@ -981,6 +981,10 @@ export Option (none some)
 instance {α} : Inhabited (Option α) where
   default := none
 
+@[macroInline] def Option.getD : Option α → α → α
+  | some x, _ => x
+  | none,   e => e
+
 inductive List (α : Type u) where
   | nil : List α
   | cons (head : α) (tail : List α) : List α
@@ -1807,6 +1811,9 @@ def SourceInfo.fromRef (ref : Syntax) : SourceInfo :=
   | some pos, some tailPos => SourceInfo.synthetic pos tailPos
   | _,        _            => SourceInfo.none
 
+def mkAtom (val : String) : Syntax :=
+  Syntax.atom SourceInfo.none val
+
 def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
   Syntax.atom src.getHeadInfo val
 

tests/lean/interactive/plainGoal.lean.expected.out

@@ -46,8 +46,7 @@
  "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = m"]}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 25, "character": 13}}
-{"rendered": "```lean\nn m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n\n```",
- "goals": ["n m : Nat\nh1 : n = m\nh2 : m = 0\n⊢ 0 = n"]}
+{"rendered": "no goals", "goals": []}
 {"textDocument": {"uri": "file://plainGoal.lean"},
  "position": {"line": 32, "character": 3}}
 {"rendered": "```lean\ncase zero\n⊢ 0 + Nat.zero = Nat.zero\n```",