Update Std/Tactic/TryThis.lean

leanprover-community · Aug 9, 2023 · ed72df0 · ed72df0
1 parent db96f32
commit ed72df0
Showing 1 changed file with 1 addition and 7 deletions.
diff --git a/Std/Tactic/TryThis.lean b/Std/Tactic/TryThis.lean
@@ -184,13 +184,7 @@ def addRewriteSuggestion (ref : Syntax) (rules : List (Expr × Bool))
     let loc ← loc?.mapM fun loc => do `(location| at $(← delab loc):term)
     `(tactic| rw [$rules_stx,*] $(loc)?)
 
-  let mut tacMsg :=
-    let rulesMsg := MessageData.sbracket <| MessageData.joinSep
-      (rules.map fun ⟨e, symm⟩ => (if symm then "← " else "") ++ m!"{e}") ", "
-    if let some loc := loc? then
-      m!"rw {rulesMsg} at {loc}"
-    else
-      m!"rw {rulesMsg}"
+  let mut tacMsg := m!"{tac}"
   let mut extraMsg := ""
   if let some type := type? then
     tacMsg := tacMsg ++ m!"\n-- {type}"