chore: restore %$tk

add missing prelude

src/Init/Tactics.lean

@@ -1306,6 +1306,26 @@ used when closing the goal.
 -/
 syntax (name := apply?) "apply?" (" using " (colGt term),+)? : tactic
 
+/--
+`show_term tac` runs `tac`, then prints the generated term in the form
+"exact X Y Z" or "refine X ?_ Z" if there are remaining subgoals.
+
+(For some tactics, the printed term will not be human readable.)
+-/
+syntax (name := showTerm) "show_term " tacticSeq : tactic
+
+/--
+`show_term e` elaborates `e`, then prints the generated term.
+-/
+macro (name := showTermElab) tk:"show_term " t:term : term =>
+  `(term| no_implicit_lambda% (show_term_elab%$tk $t))
+
+/--
+The command `by?` will print a suggestion for replacing the proof block with a proof term
+using `show_term`.
+-/
+macro (name := by?) tk:"by?" t:tacticSeq : term => `(show_term%$tk by%$tk $t)
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/Tactic.lean

@@ -37,3 +37,4 @@ import Lean.Elab.Tactic.NormCast
 import Lean.Elab.Tactic.Symm
 import Lean.Elab.Tactic.SolveByElim
 import Lean.Elab.Tactic.LibrarySearch
+import Lean.Elab.Tactic.ShowTerm

src/Lean/Elab/Tactic/ShowTerm.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison, Mario Carneiro
+-/
+prelude
+import Lean.Elab.ElabRules
+import Lean.Meta.Tactic.TryThis
+
+namespace Std.Tactic
+open Lean Elab Term Tactic Meta.Tactic.TryThis Parser.Tactic
+
+@[builtin_tactic showTerm] def evalShowTerm : Tactic := fun stx =>
+  match stx with
+  | `(tactic| show_term%$tk $t) => withMainContext do
+    let g ← getMainGoal
+    evalTactic t
+    addExactSuggestion tk (← instantiateMVars (mkMVar g)).headBeta (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
+/-- Implementation of `show_term` term elaborator. -/
+@[builtin_term_elab showTermElabImpl] def elabShowTerm : TermElab
+  | `(show_term_elab%$tk $t), ty => do
+    let e ← Term.elabTermEnsuringType t ty
+    Term.synthesizeSyntheticMVarsNoPostponing
+    addTermSuggestion tk (← instantiateMVars e).headBeta (origSpan? := ← getRef)
+    pure e
+  | _, _ => throwUnsupportedSyntax

src/Lean/Parser/Term.lean

@@ -817,6 +817,12 @@ def macroLastArg   := macroDollarArg <|> macroArg
 @[builtin_term_parser] def dotIdent := leading_parser
   "." >> checkNoWsBefore >> rawIdent
 
+/--
+Implementation of the `show_term` term elaborator.
+-/
+@[builtin_term_parser] def showTermElabImpl :=
+  leading_parser:leadPrec "show_term_elab " >> termParser
+
 end Term
 
 @[builtin_term_parser default+1] def Tactic.quot : Parser := leading_parser

tests/lean/run/show_term.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+/-- info: Try this: exact (n, 37) -/
+#guard_msgs in example (n : Nat) : Nat × Nat := by
+  show_term
+    constructor
+    exact n
+    exact 37
+
+/-- info: Try this: refine (?fst, ?snd) -/
+#guard_msgs in example : Nat × Nat := by
+  show_term constructor
+  repeat exact 42
+
+/-- info: Try this: fun {X} => X -/
+#guard_msgs in example : {_a : Nat} → Nat :=
+  show_term by
+    intro X
+    exact X