diff --git a/src/Init/MetaTypes.lean b/src/Init/MetaTypes.lean
index ddcf9900260d..28570d53772a 100644
--- a/src/Init/MetaTypes.lean
+++ b/src/Init/MetaTypes.lean
@@ -379,7 +379,7 @@ structure ExtractLetsConfig where
   useContext : Bool := true
   /-- If true (default: false), then once `givenNames` is exhausted, stop extracting lets. Otherwise continue extracting lets. -/
   onlyGivenNames : Bool := false
-  /-- If true (default: false), then when no name is provided for a 'let' expression, the name is used as-is without making it be inaccessible.
+  /-- If true (default: false), then when no name is provided for a `let` expression, the name is used as-is without making it be inaccessible.
   The name still might be inaccessible if the binder name was. -/
   preserveBinderNames : Bool := false
   /-- If true (default: false), lift non-extractable `let`s as far out as possible. -/
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index a1a4efc2c5c1..ece1d980731a 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -814,7 +814,7 @@ By default, the command captures all messages, but the filter condition can be a
 For example, we can select only warnings:
 ```lean
 /--
-warning: declaration uses 'sorry'
+warning: declaration uses `sorry`
 -/
 #guard_msgs(warning) in
 example : α := sorry
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index b22dbfad85f6..8f3ad5aeb630 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1370,7 +1370,7 @@ Trying to prove a false proposition:
 ```lean
 example : 1 ≠ 1 := by decide
 /-
-tactic 'decide' proved that the proposition
+Tactic `decide` proved that the proposition
   1 ≠ 1
 is false
 -/
@@ -1383,11 +1383,11 @@ opaque unknownProp : Prop
 open scoped Classical in
 example : unknownProp := by decide
 /-
-tactic 'decide' failed for proposition
+Tactic `decide` failed for proposition
   unknownProp
-since its 'Decidable' instance reduced to
-  Classical.choice ⋯
-rather than to the 'isTrue' constructor.
+because its `Decidable` instance
+  ...
+did not reduce to `isTrue` or `isFalse`.
 -/
 ```
 
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 535ea787e09d..8411b69db31d 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -30,7 +30,7 @@ structure AttributeImplCore where
   applicationTime := AttributeApplicationTime.afterTypeChecking
   deriving Inhabited
 
-/-- You can tag attributes with the 'local' or 'scoped' kind.
+/-- You can tag attributes with the `local` or `scoped` kind.
 For example: `attribute [local myattr, scoped yourattr, theirattr]`.
 
 This is used to indicate how an attribute should be scoped.
diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index 65927edbee4a..d53e3e3fa5a0 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -155,11 +155,11 @@ Recall that all structures are inductive datatypes.
 -/
 def addClass (env : Environment) (clsName : Name) : Except MessageData Environment := do
   if isClass env clsName then
-    throw m!"class has already been declared '{.ofConstName clsName true}'"
+    throw m!"class has already been declared `{.ofConstName clsName true}`"
   let some decl := env.find? clsName
-    | throw m!"unknown declaration '{clsName}'"
+    | throw m!"unknown declaration `{clsName}`"
   unless decl matches .inductInfo .. | .axiomInfo .. do
-    throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant"
+    throw m!"invalid `class`, declaration `{.ofConstName clsName}` must be inductive datatype, structure, or constant"
   let outParams ← checkOutParam 0 #[] #[] decl.type
   return classExtension.addEntry env { name := clsName, outParams }
 
diff --git a/src/Lean/Data/Json/FromToJson/Basic.lean b/src/Lean/Data/Json/FromToJson/Basic.lean
index 6c2de035748e..65ed230c0505 100644
--- a/src/Lean/Data/Json/FromToJson/Basic.lean
+++ b/src/Lean/Data/Json/FromToJson/Basic.lean
@@ -191,7 +191,7 @@ protected def _root_.Float.fromJson? : Json → Except String Float
   | (Json.str "-Infinity") => Except.ok (-1.0 / 0.0)
   | (Json.str "NaN") => Except.ok (0.0 / 0.0)
   | (Json.num jn) => Except.ok jn.toFloat
-  | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'."
+  | _ => Except.error "Expected a number or a string `Infinity`, `-Infinity`, `NaN`."
 
 instance : FromJson Float where
   fromJson? := Float.fromJson?
diff --git a/src/Lean/DocString/Parser.lean b/src/Lean/DocString/Parser.lean
index 45dd2fa2318d..a07beaf13669 100644
--- a/src/Lean/DocString/Parser.lean
+++ b/src/Lean/DocString/Parser.lean
@@ -25,7 +25,7 @@ private partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
   if s.hasError then
     return if iniPos == s.pos && n == 0 then s.restore iniSz iniPos else s
   if iniPos == s.pos then
-    return s.mkUnexpectedError "invalid 'atLeast' parser combinator application, parser did not consume anything"
+    return s.mkUnexpectedError "invalid `atLeast` parser combinator application, parser did not consume anything"
   if s.stackSize > iniSz + 1 then
     s := s.mkNode nullKind iniSz
   atLeastAux (n - 1) p c s
@@ -64,7 +64,7 @@ private partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn
     if s.hasError then
       return if iniPos == s.pos then s.restore iniSz iniPos else s
     if iniPos == s.pos then
-      return s.mkUnexpectedError "invalid 'atMost' parser combinator application, parser did not \
+      return s.mkUnexpectedError "invalid `atMost` parser combinator application, parser did not \
         consume anything"
     if s.stackSize > iniSz + 1 then
       s := s.mkNode nullKind iniSz
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index a0f6310d1263..b81e91773688 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -854,7 +854,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       let valResult ← elabTermEnsuringType valStx type
       let valResult ← mkLambdaFVars xs valResult (usedLetOnly := false)
       unless (← isDefEq val valResult) do
-        throwError "unexpected error when elaborating 'let'"
+        throwError "unexpected error when elaborating `let`"
   pure result
 
 structure LetIdDeclView where
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index c05a9deb0e25..05aacb4df0bb 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -286,7 +286,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax
   let nss ← resolveNamespace ns
   let currNamespace ← getCurrNamespace
-  if nss == [currNamespace] then throwError "invalid 'export', self export"
+  if nss == [currNamespace] then throwError "invalid `export`, self export"
   let mut aliases := #[]
   for idStx in ids do
     let id := idStx.getId
@@ -515,7 +515,7 @@ open Lean.Parser.Command.InternalSyntax in
   | `($doc:docComment add_decl_doc $id) =>
     let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
     unless ((← getEnv).getModuleIdxFor? declName).isNone do
-      throwError "invalid 'add_decl_doc', declaration is in an imported module"
+      throwError "invalid `add_decl_doc`, declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`
@@ -532,7 +532,7 @@ open Lean.Parser.Command.InternalSyntax in
       if let some idx := vars.findIdx? (· == id.getId) then
         uids := uids.push sc.varUIds[idx]!
       else
-        throwError "invalid 'include', variable `{id}` has not been declared in the current scope"
+        throwError "invalid `include`, variable `{id}` has not been declared in the current scope"
     modifyScope fun sc => { sc with
       includedVars := sc.includedVars ++ uids.toList
       omittedVars := sc.omittedVars.filter (!uids.contains ·) }
@@ -571,7 +571,7 @@ open Lean.Parser.Command.InternalSyntax in
             omittedVars := omittedVars.push uid
             omitsUsed := omitsUsed.set! idx true
           else
-            throwError "invalid 'omit', `{ldecl.userName}` has not been declared in the current scope"
+            throwError "invalid `omit`, `{ldecl.userName}` has not been declared in the current scope"
       for o in omits, used in omitsUsed do
         unless used do
           throwError "`{o}` did not match any variables in the current scope"
@@ -592,10 +592,10 @@ open Lean.Parser.Command.InternalSyntax in
   logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
 
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
-  logWarning "using 'exit' to interrupt Lean"
+  logWarning "using `exit` to interrupt Lean"
 
 @[builtin_command_elab Parser.Command.import] def elabImport : CommandElab := fun _ =>
-  throwError "invalid 'import' command, it must be used in the beginning of the file"
+  throwError "invalid `import` command, it must be used in the beginning of the file"
 
 @[builtin_command_elab Parser.Command.eoi] def elabEoi : CommandElab := fun _ =>
   return
diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean
index 87792a012ccf..b093ae709fc1 100644
--- a/src/Lean/Elab/BuiltinEvalCommand.lean
+++ b/src/Lean/Elab/BuiltinEvalCommand.lean
@@ -101,9 +101,9 @@ private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorr
     let axioms ← collectAxioms declName
     if axioms.contains ``sorryAx then
       throwError "\
-        aborting evaluation since the expression depends on the 'sorry' axiom, \
+        aborting evaluation since the expression depends on the `sorry` axiom, \
         which can lead to runtime instability and crashes.\n\n\
-        To attempt to evaluate anyway despite the risks, use the '#eval!' command."
+        To attempt to evaluate anyway despite the risks, use the `#eval!` command."
   return declName
 
 /--
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index 32a49b1f9dd9..906bac2b18c8 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -167,7 +167,7 @@ private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
     mkTacticMVar expectedType stx .term (delayOnMVars := (← getEnv).isExporting && !(← backward.proofsInPublic.getM))
   | none =>
     tryPostpone
-    throwError ("invalid 'by' tactic, expected type has not been provided")
+    throwError ("invalid `by` tactic, expected type has not been provided")
 
 @[builtin_term_elab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
   elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean
index b90a49fba3b2..b0cf1688cf33 100644
--- a/src/Lean/Elab/Calc.lean
+++ b/src/Lean/Elab/Calc.lean
@@ -45,9 +45,9 @@ def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr)
     let result := mkAppN (Lean.mkConst ``Trans.trans [u, v, w, u_1, u_2, u_3]) #[α, β, γ, r, s, t, self, a, b, c, result, step]
     let resultType := (← instantiateMVars (← inferType result)).headBeta
     unless (← getCalcRelation? resultType).isSome do
-      throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
+      throwError "invalid `calc` step, step result is not a relation{indentExpr resultType}"
     return (result, resultType)
-  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}{useDiagnosticMsg}"
+  | _ => throwError "invalid `calc` step, failed to synthesize `Trans` instance{indentExpr selfType}{useDiagnosticMsg}"
 
 /--
 Adds a type annotation to a hole that occurs immediately at the beginning of the term.
@@ -111,11 +111,11 @@ def elabCalcSteps (steps : Array CalcStepView) : TermElabM (Expr × Expr) := do
       else
         pure step.term
     let some (_, lhs, rhs) ← getCalcRelation? type |
-      throwErrorAt step.term "invalid 'calc' step, relation expected{indentExpr type}"
+      throwErrorAt step.term "invalid `calc` step, relation expected{indentExpr type}"
     if let some prevRhs := prevRhs? then
       unless (← isDefEqGuarded lhs prevRhs) do
         throwErrorAt step.term "\
-          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
+          invalid `calc` step, left-hand side is{indentD m!"{lhs} : {← inferType lhs}"}\n\
           but previous right-hand side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}"
     let proof ← withFreshMacroScope do elabTermEnsuringType step.proof type
     result? := some <| ← do
@@ -138,19 +138,19 @@ def throwCalcFailure (steps : Array CalcStepView) (expectedType result : Expr) :
         let (lhs, elhs) ← addPPExplicitToExposeDiff lhs elhs
         let (lhsTy, elhsTy) ← addPPExplicitToExposeDiff (← inferType lhs) (← inferType elhs)
         logErrorAt steps[0]!.term m!"\
-          invalid 'calc' step, left-hand side is{indentD m!"{lhs} : {lhsTy}"}\n\
+          invalid `calc` step, left-hand side is{indentD m!"{lhs} : {lhsTy}"}\n\
           but is expected to be{indentD m!"{elhs} : {elhsTy}"}"
         failed := true
       unless ← isDefEqGuarded rhs erhs do
         let (rhs, erhs) ← addPPExplicitToExposeDiff rhs erhs
         let (rhsTy, erhsTy) ← addPPExplicitToExposeDiff (← inferType rhs) (← inferType erhs)
         logErrorAt steps.back!.term m!"\
-          invalid 'calc' step, right-hand side is{indentD m!"{rhs} : {rhsTy}"}\n\
+          invalid `calc` step, right-hand side is{indentD m!"{rhs} : {rhsTy}"}\n\
           but is expected to be{indentD m!"{erhs} : {erhsTy}"}"
         failed := true
       if failed then
         throwAbortTerm
-  throwTypeMismatchError "'calc' expression" expectedType resultType result
+  throwTypeMismatchError "`calc` expression" expectedType resultType result
 
 /-!
 Warning! It is *very* tempting to try to improve `calc` so that it makes use of the expected type
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index e248fd5ff76a..aabd3d0d9228 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -226,7 +226,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
   let name := view.name
   let isRootName := (`_root_).isPrefixOf name
   if name == `_root_ then
-    throwError "invalid declaration name `_root_`, `_root_` is a prefix used to refer to the 'root' namespace"
+    throwError "invalid declaration name `_root_`, `_root_` is a prefix used to refer to the `root` namespace"
   let declName := if isRootName then { view with name := name.replacePrefix `_root_ Name.anonymous }.review else currNamespace ++ shortName
   if isRootName then
     let .str p s := name | throwError "invalid declaration name `{name}`"
diff --git a/src/Lean/Elab/Do/Legacy.lean b/src/Lean/Elab/Do/Legacy.lean
index 0241bed712f5..a70887e94729 100644
--- a/src/Lean/Elab/Do/Legacy.lean
+++ b/src/Lean/Elab/Do/Legacy.lean
@@ -33,7 +33,7 @@ private def getDoSeq (doStx : Syntax) : Syntax :=
   doStx[1]
 
 def elabLiftMethod : TermElab := fun stx _ =>
-  throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a 'do' expression"
+  throwErrorAt stx "invalid use of `(<- ...)`, must be nested inside a `do` expression"
 
 /-- Return true if we should not lift `(<- ...)` actions nested in the syntax nodes with the given kind. -/
 private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 8786d254bc88..3c436f33cb9d 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -38,7 +38,7 @@ private def throwForInFailure (forInInstance : Expr) : TermElabM Expr :=
         let forInInstance ← try
           mkAppM ``ForIn #[m, colType, elemType]
         catch _ =>
-          tryPostpone; throwError "failed to construct 'ForIn' instance for collection{indentExpr colType}\nand monad{indentExpr m}"
+          tryPostpone; throwError "failed to construct `ForIn` instance for collection{indentExpr colType}\nand monad{indentExpr m}"
         match (← trySynthInstance forInInstance) with
         | .some inst =>
           let forInFn ← mkConst ``forIn
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 1e8a6138598e..63fda15f5d6b 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -38,11 +38,11 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
     let attrs ← if attrOptStx.isNone then pure #[] else elabDeclAttrs attrOptStx[0]
     let decl := attrDeclStx[2][0]
     if decl.isOfKind `Lean.Parser.Term.letPatDecl then
-      throwErrorAt decl "patterns are not allowed in 'let rec' expressions"
+      throwErrorAt decl "patterns are not allowed in `let rec` expressions"
     else if decl.isOfKind ``Lean.Parser.Term.letIdDecl || decl.isOfKind ``Lean.Parser.Term.letEqnsDecl then
       let declId := decl[0][0]
       unless declId.isIdent do
-        throwErrorAt declId "'let rec' expressions must be named"
+        throwErrorAt declId "`let rec` expressions must be named"
       let shortDeclName := declId.getId
       let parentName? ← getDeclName?
       let declName := parentName?.getD Name.anonymous ++ shortDeclName
@@ -58,7 +58,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do
       let typeStx := expandOptType declId decl[2]
       let (type, binderIds) ← elabBindersEx binders fun xs => do
           let type ← elabType typeStx
-          registerCustomErrorIfMVar type typeStx "failed to infer 'let rec' declaration type"
+          registerCustomErrorIfMVar type typeStx "failed to infer `let rec` declaration type"
           let (binderIds, xs) := xs.unzip
           let type ← mkForallFVars xs type
           pure (type, binderIds)
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 97a7e98b6257..06605fcd94ad 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -506,7 +506,7 @@ partial def normalize (e : Expr) : M Expr := do
         let p := e.getArg! 2
         let h := e.getArg! 3
         unless x.consumeMData.isFVar && h.consumeMData.isFVar do
-          throwError "Unexpected occurrence of auxiliary declaration 'namedPattern'"
+          throwError "Unexpected occurrence of auxiliary declaration `namedPattern`"
         addVar x
         let p ← normalize p
         addVar h
@@ -608,7 +608,7 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
         let p ← toPattern <| e.getArg! 2
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
-        | _,           _           => throwError "Unexpected occurrence of auxiliary declaration 'namedPattern'"
+        | _,           _           => throwError "Unexpected occurrence of auxiliary declaration `namedPattern`"
       else if (← isMatchValue e) then
         return Pattern.val (← normLitValue e)
       else if e.isFVar then
@@ -1068,7 +1068,7 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
   let mut generalizing? := generalizing?
   if !matchOptMotive.isNone then
     if generalizing? == some true then
-      throwError "The '(generalizing := true)' parameter is not supported when the 'match' motive is explicitly provided"
+      throwError "The `(generalizing := true)` parameter is not supported when the `match` motive is explicitly provided"
     generalizing? := some false
   let (discrs, matchType, altLHSS, isDep, rhss) ← commitIfDidNotPostpone do
     let ⟨discrs, matchType, isDep, altViews⟩ ← elabMatchTypeAndDiscrs discrStxs matchOptMotive altViews expectedType
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 34f086359609..d637960849f1 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -91,17 +91,17 @@ private def checkKinds (k₁ k₂ : DefKind) : TermElabM Unit := do
 
 private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewElabHeader) : TermElabM Unit := do
   if newHeader.kind.isTheorem && newHeader.modifiers.isUnsafe then
-    throwError "'unsafe' theorems are not allowed"
+    throwError "`unsafe` theorems are not allowed"
   if newHeader.kind.isTheorem && newHeader.modifiers.isPartial then
-    throwError "'partial' theorems are not allowed, 'partial' is a code generation directive"
+    throwError "`partial` theorems are not allowed, `partial` is a code generation directive"
   if newHeader.kind.isTheorem && newHeader.modifiers.isMeta then
-    throwError "'meta' theorems are not allowed, 'meta' is a code generation directive"
+    throwError "`meta` theorems are not allowed, `meta` is a code generation directive"
   if newHeader.kind.isTheorem && newHeader.modifiers.isNoncomputable then
-    throwError "'theorem' subsumes 'noncomputable', code is not generated for theorems"
+    throwError "`theorem` subsumes `noncomputable`, code is not generated for theorems"
   if newHeader.modifiers.isNoncomputable && newHeader.modifiers.isPartial then
-    throwError "'noncomputable partial' is not allowed"
+    throwError "`noncomputable partial` is not allowed"
   if newHeader.modifiers.isPartial && newHeader.modifiers.isUnsafe then
-    throwError "'unsafe' subsumes 'partial'"
+    throwError "`unsafe` subsumes `partial`"
   if h : 0 < prevHeaders.size then
     let firstHeader := prevHeaders[0]
     try
@@ -1484,7 +1484,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do
     let d := ds[i]
     let modifiers ← elabModifiers ⟨d[0]⟩
     if ds.size > 1 && modifiers.isNonrec then
-      throwErrorAt d "invalid use of 'nonrec' modifier in 'mutual' block"
+      throwErrorAt d "invalid use of `nonrec` modifier in `mutual` block"
     let mut view ←
       withExporting (isExporting := modifiers.visibility.isInferredPublic (← getEnv)) do
         mkDefView modifiers d[1]
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index ecf2dccf5469..94b8dc34daa2 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -27,7 +27,7 @@ private def addAndCompilePartial
       let value ← if useSorry then
         mkLambdaFVars xs (← withRef preDef.ref <| mkLabeledSorry type (synthetic := true) (unique := true))
       else
-        let msg := m!"failed to compile 'partial' definition `{preDef.declName}`"
+        let msg := m!"failed to compile `partial` definition `{preDef.declName}`"
         liftM <| mkInhabitantFor msg xs type
       addNonRec docCtx { preDef with
         kind  := DefKind.«opaque»
diff --git a/src/Lean/Elab/PreDefinition/MkInhabitant.lean b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
index 4233a84252c0..c614676ae31d 100644
--- a/src/Lean/Elab/PreDefinition/MkInhabitant.lean
+++ b/src/Lean/Elab/PreDefinition/MkInhabitant.lean
@@ -70,7 +70,7 @@ def mkInhabitantFor (failedToMessage : MessageData) (xs : Array Expr) (type : Ex
           instances for the return type, while making every parameter into a local '{.ofConstName ``Inhabited}' instance.\n\
         - It tries unfolding the return type.\n\
         \n\
-        If the return type is defined using the 'structure' or 'inductive' command, \
-        you can try adding a 'deriving Nonempty' clause to it."
+        If the return type is defined using the `structure` or `inductive` command, \
+        you can try adding a `deriving Nonempty` clause to it."
 
 end Lean.Elab
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index a6c817a4c670..d2a1ee54fd62 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -549,7 +549,7 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter
   match discrs, alts with
   | [],            ([], rhs)::_ => pure rhs  -- nothing left to match
   | _,             []           =>
-   logError "non-exhaustive 'match' (syntax)"
+   logError "non-exhaustive `match` (syntax)"
    pure Syntax.missing
   | discr::discrs, alt::alts    => do
     let info ← getHeadInfo alt
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 4b305273a223..3fc70517c695 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -2384,7 +2384,7 @@ def displayStats (env : Environment) : IO Unit := do
   IO.println ("trust level:                           " ++ toString env.header.trustLevel);
   IO.println ("number of extensions:                  " ++ toString env.base.private.extensions.size);
   pExtDescrs.forM fun extDescr => do
-    IO.println ("extension '" ++ toString extDescr.name ++ "'")
+    IO.println ("extension `" ++ toString extDescr.name ++ "`")
     -- get state from `checked` at the end if `async`; it would otherwise panic
     let mut asyncMode := extDescr.toEnvExtension.asyncMode
     if asyncMode matches .async _ then
@@ -2417,7 +2417,7 @@ such as in `#eval`.
   evalConstCore α env opts constName
 
 private def throwUnexpectedType {α} (typeName : Name) (constName : Name) : ExceptT String Id α :=
-  throw ("unexpected type at '" ++ toString constName ++ "', `" ++ toString typeName ++ "` expected")
+  throw ("unexpected type at `" ++ toString constName ++ "`, `" ++ toString typeName ++ "` expected")
 
 /--
 Replays the difference between `newEnv` and `oldEnv` onto `dest`: the set of constants in `newEnv`
diff --git a/src/Lean/InternalExceptionId.lean b/src/Lean/InternalExceptionId.lean
index c0e9de6e0fe5..2553b66a3d24 100644
--- a/src/Lean/InternalExceptionId.lean
+++ b/src/Lean/InternalExceptionId.lean
@@ -28,7 +28,7 @@ This method is usually invoked using the `initialize` command.
 -/
 def registerInternalExceptionId (name : Name) : IO InternalExceptionId := do
   let exs ← internalExceptionsRef.get
-  if exs.contains name then throw <| IO.userError s!"invalid internal exception id, '{name}' has already been used"
+  if exs.contains name then throw <| IO.userError s!"invalid internal exception id, `{name}` has already been used"
   let nextIdx := exs.size
   internalExceptionsRef.modify fun a => a.push name
   pure { idx := nextIdx }
diff --git a/src/Lean/Meta/AbstractNestedProofs.lean b/src/Lean/Meta/AbstractNestedProofs.lean
index 9ad124f04d8e..529ed0449342 100644
--- a/src/Lean/Meta/AbstractNestedProofs.lean
+++ b/src/Lean/Meta/AbstractNestedProofs.lean
@@ -23,7 +23,7 @@ def abstractProof [Monad m] [MonadLiftT MetaM m] [MonadEnv m] [MonadOptions m] [
   let type ← postprocessType type
   /- https://github.com/leanprover/lean4/issues/10196
      If we use the cache when the proof contains `sorry`,
-     then we may fail to get a "declaration contains 'sorry'" warning for the current declaration. -/
+     then we may fail to get a "declaration uses `sorry`" warning for the current declaration. -/
   let cache := cache && !proof.hasSorry
   /- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to
     identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step.
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index d8fbe88cae45..4d62949a8ca0 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -557,7 +557,7 @@ partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
           pure none
       match r? with
       | some r => pure r
-      | none   => throwAppBuilderException `mkProjection ("invalid field name '" ++ toString fieldName ++ "' for" ++ hasTypeMsg s type)
+      | none   => throwAppBuilderException `mkProjection ("invalid field name `" ++ toString fieldName ++ "` for" ++ hasTypeMsg s type)
   | _ => throwAppBuilderException `mkProjection ("structure expected" ++ hasTypeMsg s type)
 
 private def mkListLitAux (nil : Expr) (cons : Expr) : List Expr → Expr
diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean
index f4306fa1c628..a9fa8cb668b9 100644
--- a/src/Lean/Meta/Match/Basic.lean
+++ b/src/Lean/Meta/Match/Basic.lean
@@ -291,7 +291,7 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
         let p ← toPattern <| e.getArg! 2
         match e.getArg! 1, e.getArg! 3 with
         | Expr.fvar x, Expr.fvar h => return Pattern.as x p h
-        | _,           _   => throwError "Unexpected occurrence of auxiliary declaration 'namedPattern'"
+        | _,           _   => throwError "Unexpected occurrence of auxiliary declaration `namedPattern`"
       else if (← isMatchValue e) then
         return Pattern.val e
       else if e.isFVar then
diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean
index e5058362d9a3..fdd269f2f0ef 100644
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@@ -192,7 +192,7 @@ def mkSizeOfSpecLemmaName (ctorName : Name) : Name :=
   ctorName ++ `sizeOf_spec
 
 def mkSizeOfSpecLemmaInstance (ctorApp : Expr) : MetaM Expr :=
-  matchConstCtor ctorApp.getAppFn (fun _ => throwError "failed to apply 'sizeOf' spec, constructor expected{indentExpr ctorApp}") fun ctorInfo _ => do
+  matchConstCtor ctorApp.getAppFn (fun _ => throwError "failed to apply `sizeOf` spec, constructor expected{indentExpr ctorApp}") fun ctorInfo _ => do
     let ctorArgs     := ctorApp.getAppArgs
     let ctorParams   := ctorArgs[*...ctorInfo.numParams]
     let ctorFields   := ctorArgs[ctorInfo.numParams...*]
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 9bee3b41c603..5a79eb23e1c6 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -931,9 +931,9 @@ instance : ToString Exception where
   toString
     | Exception.revertFailure _ lctx toRevert varName =>
       "failed to revert "
-      ++ toString (toRevert.map (fun x => "'" ++ toString (lctx.getFVar! x).userName ++ "'"))
-      ++ ", '" ++ toString varName ++ "' depends on them, and it is an auxiliary declaration created by the elaborator"
-      ++ " (possible solution: use tactic 'clear' to remove '" ++ toString varName ++ "' from local context)"
+      ++ toString (toRevert.map (fun x => "`" ++ toString (lctx.getFVar! x).userName ++ "`"))
+      ++ ", `" ++ toString varName ++ "` depends on them, and it is an auxiliary declaration created by the elaborator"
+      ++ " (possible solution: use tactic `clear` to remove `" ++ toString varName ++ "` from local context)"
 
 /--
  `MkBinding` and `elimMVarDepsAux` are mutually recursive, but `cache` is only used at `elimMVarDepsAux`.
diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 5b38ff62d808..f96cc48cbbcc 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -415,7 +415,7 @@ partial def manyAux (p : ParserFn) : ParserFn := fun c s => Id.run do
   if s.hasError then
     return if iniPos == s.pos then s.restore iniSz iniPos else s
   if iniPos == s.pos then
-    return s.mkUnexpectedError "invalid 'many' parser combinator application, parser did not consume anything"
+    return s.mkUnexpectedError "invalid `many` parser combinator application, parser did not consume anything"
   if s.stackSize > iniSz + 1 then
     s := s.mkNode nullKind iniSz
   manyAux p c s
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index e7ca5cd63db8..2bca4483556f 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -505,7 +505,7 @@ causes an error if the universe has not been declared previously.
 ```lean
 def L₁.{u} := List (Type u)
 
--- def L₂ := List (Type u) -- error: `unknown universe level 'u'`
+-- def L₂ := List (Type u) -- error: unknown universe level `u`
 
 universe u
 def L₃ := List (Type u)
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index ffa77e20af34..0e40102b5930 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -64,7 +64,7 @@ def notFollowedByRedefinedTermToken :=
   -- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
   notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
       "do" <|> "dbg_trace" <|> "assert!" <|> "debug_assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
-    "token at 'do' element"
+    "token at `do` element"
 
 @[builtin_doElem_parser] def doLet      := leading_parser
   "let " >> optional "mut " >> letDecl
@@ -152,9 +152,9 @@ def doIfCond    :=
 -- current category call)
 @[builtin_doElem_parser] def doIf := leading_parser withResetCache <| withPositionAfterLinebreak <| ppRealGroup <|
   ppRealFill (ppIndent ("if " >> doIfCond >> " then") >> ppSpace >> doSeq) >>
-  many (checkColGe "'else if' in 'do' must be indented" >>
+  many (checkColGe "`else if` in `do` must be indented" >>
     group (ppDedent ppSpace >> ppRealFill (elseIf >> doIfCond >> " then " >> doSeq))) >>
-  optional (checkColGe "'else' in 'do' must be indented" >>
+  optional (checkColGe "`else` in `do` must be indented" >>
     ppDedent ppSpace >> ppRealFill ("else " >> doSeq))
 @[builtin_doElem_parser] def doUnless := leading_parser
   "unless " >> withForbidden "do" termParser >> " do " >> doSeq
@@ -243,7 +243,7 @@ The second `notFollowedBy` prevents this problem.
 @[builtin_doElem_parser] def doExpr   := leading_parser
   notFollowedByRedefinedTermToken >> termParser >>
   notFollowedBy (symbol ":=" <|> leftArrow)
-    "unexpected token after 'expr' in 'do' block"
+    "unexpected token after `expr` in `do` block"
 @[builtin_doElem_parser] def doNested := leading_parser
   "do " >> doSeq
 
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 86a304be4f25..875fac15b77f 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -419,7 +419,7 @@ def categoryParserFnImpl (catName : Name) : ParserFn := fun ctx s =>
   match getCategory categories catName with
   | some cat =>
     prattParser catName cat.tables cat.behavior (mkCategoryAntiquotParserFn catName) ctx s
-  | none     => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
+  | none     => s.mkUnexpectedError ("unknown parser category `" ++ toString catName ++ "`")
 
 builtin_initialize
   categoryParserFnRef.set categoryParserFnImpl
diff --git a/src/Lean/Shell.lean b/src/Lean/Shell.lean
index e39a8b9f94ec..b7a0c7d2d7df 100644
--- a/src/Lean/Shell.lean
+++ b/src/Lean/Shell.lean
@@ -147,7 +147,7 @@ def displayHelp (useStderr : Bool) : IO Unit := do
   out.putStrLn    "  -v, --version          display version information"
   out.putStrLn    "  -V, --short-version    display short version number"
   out.putStrLn    "  -g, --githash          display the git commit hash number used to build this binary"
-  out.putStrLn    "      --run <file>       call the 'main' definition in the given file with the remaining arguments"
+  out.putStrLn    "      --run <file>       call the `main` definition in the given file with the remaining arguments"
   out.putStrLn    "  -o, --o=oname          create olean file"
   out.putStrLn    "  -i, --i=iname          create ilean file"
   out.putStrLn    "  -c, --c=fname          name of the C output file"
diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean
index 1b80a1b03aa1..d029a61fafc2 100644
--- a/src/Lean/SubExpr.lean
+++ b/src/Lean/SubExpr.lean
@@ -81,7 +81,7 @@ def all (pred : Nat → Bool) (p : Pos) : Bool :=
 
 def append : Pos → Pos → Pos := foldl push
 
-/-- Creates a subexpression `Pos` from an array of 'coordinates'.
+/-- Creates a subexpression `Pos` from an array of `coordinates`.
 Each coordinate is a number {0,1,2} expressing which child subexpression should be explored.
 The first coordinate in the array corresponds to the root of the expression tree.  -/
 def ofArray (ps : Array Nat) : Pos :=
diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean
index a194e3f7c2ad..b781be11e92a 100644
--- a/src/Lean/Util/PPExt.lean
+++ b/src/Lean/Util/PPExt.lean
@@ -25,7 +25,7 @@ register_builtin_option pp.raw.maxDepth : Nat := {
 }
 register_builtin_option pp.rawOnError : Bool := {
   defValue := false
-  descr    := "(pretty printer) fallback to 'raw' printer when pretty printer fails"
+  descr    := "(pretty printer) fallback to \"raw\" printer when pretty printer fails"
 }
 
 structure PPContext where
diff --git a/tests/lean/440.lean.expected.out b/tests/lean/440.lean.expected.out
index 73302decb627..9941a93a5c25 100644
--- a/tests/lean/440.lean.expected.out
+++ b/tests/lean/440.lean.expected.out
@@ -6,6 +6,6 @@ context:
 x : Nat
 ⊢ Nat
 f (x : Nat) : Nat
-440.lean:11:0-11:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
+440.lean:11:0-11:5: error: aborting evaluation since the expression depends on the `sorry` axiom, which can lead to runtime instability and crashes.
 
-To attempt to evaluate anyway despite the risks, use the '#eval!' command.
+To attempt to evaluate anyway despite the risks, use the `#eval!` command.
diff --git a/tests/lean/Process.lean.expected.out b/tests/lean/Process.lean.expected.out
index 28b40f32d920..f65f9abc7f5e 100644
--- a/tests/lean/Process.lean.expected.out
+++ b/tests/lean/Process.lean.expected.out
@@ -7,6 +7,6 @@
 0
 0
 0
-"<stdin>:1:0: warning: using 'exit' to interrupt Lean\n"
+"<stdin>:1:0: warning: using `exit` to interrupt Lean\n"
 none
 some 0
diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out
index 2a97d3d8d7dc..079a698c2c59 100644
--- a/tests/lean/calcErrors.lean.expected.out
+++ b/tests/lean/calcErrors.lean.expected.out
@@ -4,17 +4,17 @@ has type
   ?m = ?m
 but is expected to have type
   b + b = 0 + c + b
-calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand side is
+calcErrors.lean:13:8-13:29: error: invalid `calc` step, left-hand side is
   0 + c + b : Nat
 but previous right-hand side is
   b + b : Nat
-calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
+calcErrors.lean:24:8-24:11: error: invalid `calc` step, relation expected
   p a
-calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
+calcErrors.lean:31:8-31:13: error: invalid `calc` step, failed to synthesize `Trans` instance
   Trans p p ?m
 
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-calcErrors.lean:40:7-40:12: error: invalid 'calc' step, left-hand side is
+calcErrors.lean:40:7-40:12: error: invalid `calc` step, left-hand side is
   γ : Sort u_1
 but previous right-hand side is
   b : β
diff --git a/tests/lean/class_def_must_fail.lean.expected.out b/tests/lean/class_def_must_fail.lean.expected.out
index ef5d4e31b64c..33bbe314390f 100644
--- a/tests/lean/class_def_must_fail.lean.expected.out
+++ b/tests/lean/class_def_must_fail.lean.expected.out
@@ -1,2 +1,2 @@
-class_def_must_fail.lean:2:2-2:7: error: invalid 'class', declaration 'Foo' must be inductive datatype, structure, or constant
-class_def_must_fail.lean:7:11-7:16: error: invalid 'class', declaration 'Bla' must be inductive datatype, structure, or constant
+class_def_must_fail.lean:2:2-2:7: error: invalid `class`, declaration 'Foo' must be inductive datatype, structure, or constant
+class_def_must_fail.lean:7:11-7:16: error: invalid `class`, declaration 'Bla' must be inductive datatype, structure, or constant
diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out
index 84d505e216c4..0d07c12e789e 100644
--- a/tests/lean/docStr.lean.expected.out
+++ b/tests/lean/docStr.lean.expected.out
@@ -189,4 +189,4 @@ g.foo :=
                         charUtf16 := 44,
                         endPos := { line := 42, column := 47 },
                         endCharUtf16 := 47 } }
-docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module
+docStr.lean:106:0-107:20: error: invalid `add_decl_doc`, declaration is in an imported module
diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out
index cae688ca30f8..d4ebaab87d62 100644
--- a/tests/lean/evalSorry.lean.expected.out
+++ b/tests/lean/evalSorry.lean.expected.out
@@ -7,9 +7,9 @@ but is expected to have type
   Nat
 in the application
   f x
-evalSorry.lean:7:0-7:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
+evalSorry.lean:7:0-7:5: error: aborting evaluation since the expression depends on the `sorry` axiom, which can lead to runtime instability and crashes.
 
-To attempt to evaluate anyway despite the risks, use the '#eval!' command.
-evalSorry.lean:11:0-11:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
+To attempt to evaluate anyway despite the risks, use the `#eval!` command.
+evalSorry.lean:11:0-11:5: error: aborting evaluation since the expression depends on the `sorry` axiom, which can lead to runtime instability and crashes.
 
-To attempt to evaluate anyway despite the risks, use the '#eval!' command.
+To attempt to evaluate anyway despite the risks, use the `#eval!` command.
diff --git a/tests/lean/exitAfterParseError.lean.expected.out b/tests/lean/exitAfterParseError.lean.expected.out
index 619c1e8c62cd..e91d5dd225fe 100644
--- a/tests/lean/exitAfterParseError.lean.expected.out
+++ b/tests/lean/exitAfterParseError.lean.expected.out
@@ -1,2 +1,2 @@
 exitAfterParseError.lean:3:7-5:5: error: unexpected token '#exit'; expected ':=', 'where' or '|'
-exitAfterParseError.lean:5:0-5:5: warning: using 'exit' to interrupt Lean
+exitAfterParseError.lean:5:0-5:5: warning: using `exit` to interrupt Lean
diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out
index 2d4f6261d494..8af4919657f6 100644
--- a/tests/lean/holeErrors.lean.expected.out
+++ b/tests/lean/holeErrors.lean.expected.out
@@ -22,4 +22,4 @@ holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argume
   @id ?m
 context:
 ⊢ Sort u
-holeErrors.lean:19:8-19:9: error: failed to infer 'let rec' declaration type
+holeErrors.lean:19:8-19:9: error: failed to infer `let rec` declaration type
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index b99beb2399cc..181db1e44140 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -30,4 +30,4 @@ f : {α : Type} → {β : ?m a} → α → α := ⋯
 ⊢ ?m a
 holes.lean:18:9-18:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `β`
 holes.lean:21:12-21:14: error(lean.inferDefTypeFailed): Failed to infer type of definition `f7`
-holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type
+holes.lean:25:8-25:11: error: failed to infer `let rec` declaration type
diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out
index a94982e14bf4..565e1dd7d90f 100644
--- a/tests/lean/macroStack.lean.expected.out
+++ b/tests/lean/macroStack.lean.expected.out
@@ -8,7 +8,7 @@ while expanding
   (x > 0)
 while expanding
   if h : (x > 0) then 1 else 0
-macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
+macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested inside a `do` expression
 macroStack.lean:17:0-17:6: error: failed to synthesize instance of type class
   HAdd Nat String ?m
 
diff --git a/tests/lean/match2.lean.expected.out b/tests/lean/match2.lean.expected.out
index 715b88d9c40e..b98da3d52d8a 100644
--- a/tests/lean/match2.lean.expected.out
+++ b/tests/lean/match2.lean.expected.out
@@ -15,4 +15,4 @@ true
 false
 false
 ---- Foo 3
-match2.lean:83:0-85:21: error: The '(generalizing := true)' parameter is not supported when the 'match' motive is explicitly provided
+match2.lean:83:0-85:21: error: The `(generalizing := true)` parameter is not supported when the `match` motive is explicitly provided
diff --git a/tests/lean/nonfatalattrs.lean.expected.out b/tests/lean/nonfatalattrs.lean.expected.out
index 6cc8d2771c79..c449827cc05c 100644
--- a/tests/lean/nonfatalattrs.lean.expected.out
+++ b/tests/lean/nonfatalattrs.lean.expected.out
@@ -1,4 +1,4 @@
 nonfatalattrs.lean:6:2-6:19: error: Unknown attribute `[attrUnimplementedattr]`
 foo : Nat
-nonfatalattrs.lean:11:12-11:17: error: invalid 'class', declaration 'bar.bar' must be inductive datatype, structure, or constant
+nonfatalattrs.lean:11:12-11:17: error: invalid `class`, declaration `bar.bar` must be inductive datatype, structure, or constant
 bar : Nat
diff --git a/tests/lean/root.lean.expected.out b/tests/lean/root.lean.expected.out
index 371e236809ec..2ecbd75f08b7 100644
--- a/tests/lean/root.lean.expected.out
+++ b/tests/lean/root.lean.expected.out
@@ -1,6 +1,6 @@
 Bla.f (x : Nat) : Nat
 root.lean:21:14-21:22: error: protected declarations must be in a namespace
-root.lean:29:4-29:10: error: invalid declaration name `_root_`, `_root_` is a prefix used to refer to the 'root' namespace
+root.lean:29:4-29:10: error: invalid declaration name `_root_`, `_root_` is a prefix used to refer to the `root` namespace
 root.lean:31:0-31:32: error: invalid namespace `_root_`, `_root_` is a reserved namespace
 root.lean:33:0-33:34: error: invalid namespace `f._root_`, `_root_` is a reserved namespace
 root.lean:35:14-35:22: error: protected declarations must be in a namespace
diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean
index ce4e383fda9a..aeb68bfcf69b 100644
--- a/tests/lean/run/1697.lean
+++ b/tests/lean/run/1697.lean
@@ -8,9 +8,9 @@ is false
 #eval show Nat from False.elim (by decide)
 
 /--
-error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
+error: aborting evaluation since the expression depends on the `sorry` axiom, which can lead to runtime instability and crashes.
 
-To attempt to evaluate anyway despite the risks, use the '#eval!' command.
+To attempt to evaluate anyway despite the risks, use the `#eval!` command.
 ---
 warning: declaration uses `sorry`
 -/
diff --git a/tests/lean/run/3713.lean b/tests/lean/run/3713.lean
index 5884ff62d6bb..5de22469da71 100644
--- a/tests/lean/run/3713.lean
+++ b/tests/lean/run/3713.lean
@@ -5,7 +5,7 @@ def somethingBad : MetaM Nat := do
   IO.println "oh no"
   return 1
 
-/-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression -/
+/-- error: invalid use of `(<- ...)`, must be nested inside a `do` expression -/
 #guard_msgs in
 #eval show MetaM Unit from do
   let t := if false then ← somethingBad else 9
@@ -13,7 +13,7 @@ def somethingBad : MetaM Nat := do
 def foo : MetaM Bool :=
   return false
 
-/-- error: invalid use of `(<- ...)`, must be nested inside a 'do' expression -/
+/-- error: invalid use of `(<- ...)`, must be nested inside a `do` expression -/
 #guard_msgs in
 #eval show MetaM Unit from do
   let t := if (← foo) then ← somethingBad else 9
diff --git a/tests/lean/run/4318.lean b/tests/lean/run/4318.lean
index 648411f339a8..120d12afa76d 100644
--- a/tests/lean/run/4318.lean
+++ b/tests/lean/run/4318.lean
@@ -11,7 +11,7 @@ Term-mode `calc`. Errors about LHS and RHS not matching expected type.
 -/
 
 /--
-error: invalid 'calc' step, left-hand side is
+error: invalid `calc` step, left-hand side is
   1 + n - n : Nat
 but is expected to be
   0 : Nat
@@ -22,7 +22,7 @@ example (n : Nat) : 0 = 1 :=
     1 + n - n = 1 := testSorry
 
 /--
-error: invalid 'calc' step, right-hand side is
+error: invalid `calc` step, right-hand side is
   n - n : Nat
 but is expected to be
   1 : Nat
@@ -33,7 +33,7 @@ example (n : Nat) : 0 = 1 :=
     0 = n - n := testSorry
 
 /--
-error: 'calc' expression has type
+error: `calc` expression has type
   0 = 1
 but is expected to have type
   0 < 1
@@ -47,7 +47,7 @@ example : 0 < 1 :=
 Tactic-mode `calc`. LHS failure.
 -/
 /--
-error: invalid 'calc' step, left-hand side is
+error: invalid `calc` step, left-hand side is
   1 + n - n : Nat
 but is expected to be
   0 : Nat
@@ -70,7 +70,7 @@ example (n : Nat) : 0 ≤ 1 := by
 Tactic mode `calc`. Calc extension fails due to expected type mismatch, so report original failure.
 -/
 /--
-error: 'calc' expression has type
+error: `calc` expression has type
   0 < n - n
 but is expected to have type
   0 ≤ 1
@@ -84,7 +84,7 @@ example (n : Nat) : 0 ≤ 1 := by
 Tactic mode `calc`. Calc extension fails due to nontransitivity, so report original failure.
 -/
 /--
-error: invalid 'calc' step, right-hand side is
+error: invalid `calc` step, right-hand side is
   1 : Nat
 but is expected to be
   2 : Nat
diff --git a/tests/lean/run/forInColErr.lean b/tests/lean/run/forInColErr.lean
index 532e0e516a10..460ed752c4f1 100644
--- a/tests/lean/run/forInColErr.lean
+++ b/tests/lean/run/forInColErr.lean
@@ -1,7 +1,7 @@
 set_option pp.mvars.anonymous false
 
 /--
-error: failed to construct 'ForIn' instance for collection
+error: failed to construct `ForIn` instance for collection
   ?_
 and monad
   Id
diff --git a/tests/lean/run/partialDelta.lean b/tests/lean/run/partialDelta.lean
index e34668d63a9d..2119ef585b0c 100644
--- a/tests/lean/run/partialDelta.lean
+++ b/tests/lean/run/partialDelta.lean
@@ -38,16 +38,16 @@ partial def test3 [Nonempty α] (n : Nat) : α := test3 n
 Error message.
 -/
 /--
-error: failed to compile 'partial' definition `test4`, could not prove that the type
+error: failed to compile `partial` definition `test4`, could not prove that the type
   {α : Sort u_1} → Nat → α
 is nonempty.
 
 This process uses multiple strategies:
 - It looks for a parameter that matches the return type.
-- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
+- It tries synthesizing `Inhabited` and `Nonempty` instances for the return type, while making every parameter into a local `Inhabited` instance.
 - It tries unfolding the return type.
 
-If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
+If the return type is defined using the `structure` or `inductive` command, you can try adding a `deriving Nonempty` clause to it.
 -/
 #guard_msgs in partial def test4 (n : Nat) : α := test4 n
 
diff --git a/tests/lean/run/partial_fixpoint.lean b/tests/lean/run/partial_fixpoint.lean
index ef727dd57b8d..ee11cc869416 100644
--- a/tests/lean/run/partial_fixpoint.lean
+++ b/tests/lean/run/partial_fixpoint.lean
@@ -43,10 +43,10 @@ is nonempty.
 
 This process uses multiple strategies:
 - It looks for a parameter that matches the return type.
-- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
+- It tries synthesizing `Inhabited` and `Nonempty` instances for the return type, while making every parameter into a local `Inhabited` instance.
 - It tries unfolding the return type.
 
-If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
+If the return type is defined using the `structure` or `inductive` command, you can try adding a `deriving Nonempty` clause to it.
 -/
 #guard_msgs in
 def notinhabited (n m : Nat) : Fin n :=
@@ -60,10 +60,10 @@ is nonempty.
 
 This process uses multiple strategies:
 - It looks for a parameter that matches the return type.
-- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
+- It tries synthesizing `Inhabited` and `Nonempty` instances for the return type, while making every parameter into a local `Inhabited` instance.
 - It tries unfolding the return type.
 
-If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
+If the return type is defined using the `structure` or `inductive` command, you can try adding a `deriving Nonempty` clause to it.
 -/
 #guard_msgs in
 mutual
diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean
index 61ba914043f1..84ff7f95a9a3 100644
--- a/tests/lean/run/variable.lean
+++ b/tests/lean/run/variable.lean
@@ -118,7 +118,7 @@ end
 
 /-! illegal `omit`s -/
 
-/-- error: invalid 'omit', `α` has not been declared in the current scope -/
+/-- error: invalid `omit`, `α` has not been declared in the current scope -/
 #guard_msgs in
 variable (a : α) in
 omit α in
diff --git a/tests/lean/sanitychecks.lean.expected.out b/tests/lean/sanitychecks.lean.expected.out
index 706c58c09f0a..dfc0665a765d 100644
--- a/tests/lean/sanitychecks.lean.expected.out
+++ b/tests/lean/sanitychecks.lean.expected.out
@@ -5,23 +5,23 @@ failed to infer structural recursion:
 no parameters suitable for structural recursion
 
 well-founded recursion cannot be used, `unsound` does not take any (non-fixed) arguments
-sanitychecks.lean:4:8-4:32: error: 'partial' theorems are not allowed, 'partial' is a code generation directive
-sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
+sanitychecks.lean:4:8-4:32: error: `partial` theorems are not allowed, `partial` is a code generation directive
+sanitychecks.lean:7:7-7:31: error: `unsafe` theorems are not allowed
 sanitychecks.lean:10:0-10:23: error: failed to synthesize 'Inhabited' or 'Nonempty' instance for
   False
 
 If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
 sanitychecks.lean:18:12-18:20: error: invalid use of `partial`, `Foo.unsound3` is not a function
   False
-sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition `Foo.unsound4`, could not prove that the type
+sanitychecks.lean:20:0-20:54: error: failed to compile `partial` definition `Foo.unsound4`, could not prove that the type
   ∀ (x : Unit), False
 is nonempty.
 
 This process uses multiple strategies:
 - It looks for a parameter that matches the return type.
-- It tries synthesizing 'Inhabited' and 'Nonempty' instances for the return type, while making every parameter into a local 'Inhabited' instance.
+- It tries synthesizing `Inhabited` and `Nonempty` instances for the return type, while making every parameter into a local `Inhabited` instance.
 - It tries unfolding the return type.
 
-If the return type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
+If the return type is defined using the `structure` or `inductive` command, you can try adding a `deriving Nonempty` clause to it.
 sanitychecks.lean:22:12-22:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'
 sanitychecks.lean:25:12-25:20: error: (kernel) invalid declaration, it uses unsafe declaration 'unsafeCast'