chore: backtick identifiers in elaborator tactic messages

src/Init/Data/Random.lean

@@ -27,7 +27,7 @@ class RandomGen (g : Type u) where
      and a new generator. -/
   next  : g → Nat × g
   /--
-    The 'split' operation allows one to obtain two distinct random number
+    The `split` operation allows one to obtain two distinct random number
     generators. This is very useful in functional programs (for example, when
     passing a random number generator down to recursive calls). -/
   split : g → g × g

src/Lean/Elab/Deriving/Repr.lean

@@ -31,7 +31,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term :
   forallTelescopeReducing ctorVal.type fun xs _ => do
     let mut fields ← `(Format.nil)
     if xs.size != numParams + fieldNames.size then
-      throwError "'deriving Repr' failed, unexpected number of fields in structure"
+      throwError "`deriving Repr` failed, unexpected number of fields in structure"
     for h : i in *...fieldNames.size do
       let fieldName := fieldNames[i]
       let fieldNameLit := Syntax.mkStrLit (toString fieldName)

src/Lean/Elab/Tactic/Change.lean

@@ -79,7 +79,7 @@ the main goal. -/
         let (tgt', mvars) ← withCollectingNewGoalsFrom (elabChange (← getMainTarget) newType) (← getMainTag) `change
         liftMetaTactic fun mvarId => do
           return (← mvarId.replaceTargetDefEq tgt') :: mvars)
-      (failed := fun _ => throwError "'change' tactic failed")
+      (failed := fun _ => throwError "`change` tactic failed")
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -33,7 +33,7 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) (
     MetaM (Expr × Array (Option MVarId) × Array (Option MVarId)) := do
   let funInfo ← getFunInfoNArgs f args.size
   let some congrThm ← mkCongrSimpCore? f funInfo (← getCongrSimpKinds f funInfo) (subsingletonInstImplicitRhs := false)
-    | throwError "'congr' conv tactic failed to create congruence theorem"
+    | throwError "`congr` conv tactic failed to create congruence theorem"
   let mut eNew := f
   let mut proof := congrThm.proof
   let mut mvarIdsNew := #[]
@@ -68,7 +68,7 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) (
     | .heq | .fixedNoParam => unreachable!
   if congrThm.argKinds.size < args.size then
     if congrThm.argKinds.size == 0 then
-      throwError "'congr' conv tactic failed to create congruence theorem"
+      throwError "`congr` conv tactic failed to create congruence theorem"
     let (proof', mvarIdsNew', mvarIdsNewInsts') ←
       mkCongrThm origTag eNew args[funInfo.getArity...*] addImplicitArgs nameSubgoals
     for arg in args[funInfo.getArity...*] do
@@ -100,7 +100,7 @@ def congr (mvarId : MVarId) (addImplicitArgs := false) (nameSubgoals := true) :
     mvarId.assign proof
     return mvarIdsNew.toList ++ mvarIdsNewInsts.toList
   else
-    throwError "invalid 'congr' conv tactic, application or implication expected{indentExpr lhs}"
+    throwError "invalid `congr` conv tactic, application or implication expected{indentExpr lhs}"
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun _ => do
   replaceMainGoal <| List.filterMap id (← congr (← getMainGoal))
@@ -110,7 +110,7 @@ def congrFunN (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
   let (lhs, rhs) ← getLhsRhsCore mvarId
   let lhs := (← instantiateMVars lhs).cleanupAnnotations
   unless lhs.isApp do
-    throwError "invalid 'arg 0' conv tactic, application expected{indentExpr lhs}"
+    throwError "invalid `arg 0` conv tactic, application expected{indentExpr lhs}"
   lhs.withApp fun f xs => do
     let (g, mvarNew) ← mkConvGoalFor f
     mvarId.assign (← xs.foldlM (init := mvarNew) Meta.mkCongrFun)
@@ -250,7 +250,7 @@ def evalArg (tacticName : String) (i : Int) (explicit : Bool) : TacticM Unit :=
     let (lhs, rhs) ← getLhsRhsCore mvarId
     let lhs := (← instantiateMVars lhs).cleanupAnnotations
     let .app f a := lhs
-      | throwError "invalid 'fun' conv tactic, application expected{indentExpr lhs}"
+      | throwError "invalid `fun` conv tactic, application expected{indentExpr lhs}"
     let (g, mvarNew) ← mkConvGoalFor f
     mvarId.assign (← Meta.mkCongrFun mvarNew a)
     resolveRhs "fun" rhs (.app g a)
@@ -307,8 +307,8 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
     else
       let lhsType ← whnfD (← inferType lhs)
       unless lhsType.isForall do
-        throwError "invalid 'ext' conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
-      let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "'apply funext' unexpected result"
+        throwError "invalid `ext` conv tactic, function or arrow expected{indentD m!"{lhs} : {lhsType}"}"
+      let [mvarId] ← mvarId.apply (← mkConstWithFreshMVarLevels ``funext) | throwError "`apply funext` unexpected result"
       let userNames := if let some userName := userName? then [userName] else []
       let (_, mvarId) ← mvarId.introN 1 userNames
       markAsConvGoal mvarId

src/Lean/Elab/Tactic/Conv/Pattern.lean

@@ -132,11 +132,11 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
     let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state })
     let subgoals ← match ← state.get with
     | .all #[] | .occs _ 0 _ =>
-      throwError "'pattern' conv tactic failed, pattern was not found{indentExpr patternA.expr}"
+      throwError "`pattern` conv tactic failed, pattern was not found{indentExpr patternA.expr}"
     | .all subgoals => pure subgoals
     | .occs subgoals idx remaining =>
       if let some (i, _) := remaining.getLast? then
-        throwError "'pattern' conv tactic failed, pattern was found only {idx} times but {i+1} expected"
+        throwError "`pattern` conv tactic failed, pattern was found only {idx} times but {i+1} expected"
       pure <| (subgoals.qsort (·.1 < ·.1)).map (·.2)
     (← getRhs).mvarId!.assign result.expr
     (← getMainGoal).assign (← result.getProof)

src/Lean/Elab/Tactic/Doc.lean

@@ -35,7 +35,7 @@ open Lean.Parser.Command
   | `(«register_tactic_tag»|$[$doc:docComment]? register_tactic_tag $tag:ident $user:str) => do
     let docstring ← doc.mapM getDocStringText
     modifyEnv (knownTacticTagExt.addEntry · (tag.getId, user.getString, docstring))
-  | _ => throwError "Malformed 'register_tactic_tag' command"
+  | _ => throwError "Malformed `register_tactic_tag` command"
 
 /--
 Gets the first string token in a parser description. For example, for a declaration like

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -242,7 +242,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
       let mvarId ← mvarId.tryClear h.fvarId!
       replaceMainGoal (mvarIds' ++ [mvarId])
     else
-      throwError "'specialize' requires a term of the form `h x_1 .. x_n` where `h` appears in the local context"
+      throwError "`specialize` requires a term of the form `h x_1 .. x_n` where `h` appears in the local context"
   | _ => throwUnsupportedSyntax
 
 /--

src/Lean/Elab/Tactic/Induction.lean

@@ -18,8 +18,8 @@ public section
 
 register_builtin_option tactic.customEliminators : Bool := {
   defValue := true
-  descr    := "enable using custom eliminators in the 'induction' and 'cases' tactics \
-    defined using the '@[induction_eliminator]' and '@[cases_eliminator]' attributes"
+  descr    := "enable using custom eliminators in the `induction` and `cases` tactics \
+    defined using the `@[induction_eliminator]` and `@[cases_eliminator]` attributes"
 }
 
 end
@@ -1005,11 +1005,11 @@ def evalInduction : Tactic := fun stx =>
 
 register_builtin_option tactic.fun_induction.unfolding : Bool := {
   defValue := true
-  descr    := "if set to 'true', then 'fun_induction' and 'fun_cases' will use the “unfolding \
-    functional induction (resp. cases) principle” ('….induct_unfolding'/'….fun_cases_unfolding'), \
+  descr    := "if set to `true`, then `fun_induction` and `fun_cases` will use the \"unfolding \
+    functional induction (resp. cases) principle\" (`….induct_unfolding`/`….fun_cases_unfolding`), \
     which will attempt to replace the function goal of interest in the goal with the appropriate \
-    right-hand-side in each case. If 'false', the regular “functional induction principle” \
-    ('….induct'/'….fun_cases') is used."
+    right-hand-side in each case. If `false`, the regular \"functional induction principle\" \
+    (`….induct`/`….fun_cases`) is used."
 }
 
 /--

src/Lean/Elab/Tactic/Lets.lean

@@ -55,7 +55,7 @@ declare_config_elab elabExtractLetsConfig ExtractLetsConfig
           let ((fvars, _), mvarId) ← mvarId.extractLets givenNames config
           return (fvars, [mvarId])
         extractLetsAddVarInfo ids fvars)
-      (failed := fun _ => throwError "'extract_lets' tactic failed")
+      (failed := fun _ => throwError "`extract_lets` tactic failed")
   | _ => throwUnsupportedSyntax
 
 /-!
@@ -70,7 +70,7 @@ declare_config_elab elabLiftLetsConfig LiftLetsConfig
     withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
       (atLocal := fun h => liftMetaTactic1 fun mvarId => mvarId.liftLetsLocalDecl h config)
       (atTarget := liftMetaTactic1 fun mvarId => mvarId.liftLets config)
-      (failed := fun _ => throwError "'lift_lets' tactic failed")
+      (failed := fun _ => throwError "`lift_lets` tactic failed")
   | _ => throwUnsupportedSyntax
 
 /-!
@@ -82,7 +82,7 @@ declare_config_elab elabLiftLetsConfig LiftLetsConfig
     withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
       (atLocal := fun h => liftMetaTactic1 fun mvarId => mvarId.letToHaveLocalDecl h)
       (atTarget := liftMetaTactic1 fun mvarId => mvarId.letToHave)
-      (failed := fun _ => throwError "'let_to_have' tactic failed")
+      (failed := fun _ => throwError "`let_to_have` tactic failed")
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -248,7 +248,7 @@ where
       let (lc, prf, facts) ← asLinearCombo rhs
       let prf' : OmegaM Expr := do mkEqTrans rw (← prf)
       pure (lc, prf', facts)
-    | none => panic! "Invalid rewrite rule in 'asLinearCombo'"
+    | none => panic! "Invalid rewrite rule in `asLinearCombo`"
   handleNatCast (e i n : Expr) : OmegaM (LinearCombo × OmegaM Expr × List Expr) := do
     match n with
     | .fvar h =>

src/Lean/Elab/Tactic/Show.lean

@@ -55,11 +55,11 @@ where
       setGoals newGoals
   simpleError (p tgt : Expr) : MetaM MessageData := do
     return m!"\
-      'show' tactic failed, pattern{indentExpr p}\n\
+      `show` tactic failed, pattern{indentExpr p}\n\
       is not definitionally equal to target{indentExpr tgt}"
   manyError (p tgt : Expr) : MetaM MessageData := do
     return m!"\
-      'show' tactic failed, no goals unify with the given pattern.\n\
+      `show` tactic failed, no goals unify with the given pattern.\n\
       \n\
       In the first goal, the pattern{indentExpr p}\n\
       is not definitionally equal to the target{indentExpr tgt}\n\

src/Lean/Elab/Tactic/Try.lean

@@ -273,7 +273,7 @@ builtin_initialize registerBuiltinAttribute {
     let prio ← match stx with
       | `(attr| try_suggestion $n:num) => pure n.getNat
       | `(attr| try_suggestion) => pure 1000  -- Default priority
-      | _ => throwError "invalid 'try_suggestion' attribute syntax"
+      | _ => throwError "invalid `try_suggestion` attribute syntax"
     let attrKind := if kind == AttributeKind.local then AttributeKind.local else AttributeKind.global
     trySuggestionExtension.add {
       name := declName,

tests/lean/conv1.lean.expected.out

@@ -160,10 +160,10 @@ x y z : Nat
 
 x y z : Nat
 | y + z
-conv1.lean:248:58-248:83: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected
-conv1.lean:249:58-249:85: error: 'pattern' conv tactic failed, pattern was found only 4 times but 5 expected
-conv1.lean:250:58-250:85: error: 'pattern' conv tactic failed, pattern was found only 3 times but 5 expected
-conv1.lean:251:58-251:87: error: 'pattern' conv tactic failed, pattern was found only 2 times but 5 expected
+conv1.lean:248:58-248:83: error: `pattern` conv tactic failed, pattern was found only 4 times but 5 expected
+conv1.lean:249:58-249:85: error: `pattern` conv tactic failed, pattern was found only 4 times but 5 expected
+conv1.lean:250:58-250:85: error: `pattern` conv tactic failed, pattern was found only 3 times but 5 expected
+conv1.lean:251:58-251:87: error: `pattern` conv tactic failed, pattern was found only 2 times but 5 expected
 P Q : Nat → Nat → Nat → Prop
 h : P = Q
 h2 : Q 1 2 3
@@ -180,7 +180,7 @@ P Q : Nat → Nat → Nat → Prop
 h : P = Q
 h2 : Q 1 2 3
 | P
-conv1.lean:275:10-275:13: error: invalid 'fun' conv tactic, application expected
+conv1.lean:275:10-275:13: error: invalid `fun` conv tactic, application expected
   p
 P Q : Nat → Nat → Nat → Prop
 h : P = Q
@@ -190,5 +190,5 @@ P Q : Nat → Nat → Nat → Prop
 h : P = Q
 h2 : Q 1 2 3
 | P
-conv1.lean:287:10-287:15: error: invalid 'arg 0' conv tactic, application expected
+conv1.lean:287:10-287:15: error: invalid `arg 0` conv tactic, application expected
   p

tests/lean/run/showTactic.lean

@@ -22,7 +22,7 @@ example : x = 0 := by
 -/
 
 /--
-error: 'show' tactic failed, pattern
+error: `show` tactic failed, pattern
   x = 1
 is not definitionally equal to target
   x = 0
@@ -123,7 +123,7 @@ also weren't defeq.
 -/
 
 /--
-error: 'show' tactic failed, no goals unify with the given pattern.
+error: `show` tactic failed, no goals unify with the given pattern.
 
 In the first goal, the pattern
   x = 4