chore: backtick identifiers in core messages and tests

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. -/

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

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`.
 -/
 ```
 

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.

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 }
 

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?

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

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

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

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
 
 /--

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?)

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

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}`"

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 :=

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

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)

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

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]

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»

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