chore: use backticks instead of single quotes for identifiers in messages

This PR standardizes the formatting of identifiers in error messages, warnings, diagnostics, and documentation to use backticks instead of single quotes. For example, `'sorry'` becomes `` `sorry` ``.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <[email protected]>

Author: alok

src/Init/MetaTypes.lean

@@ -367,7 +367,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

@@ -803,7 +803,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/Lean/AddDecl.lean

@@ -68,7 +68,7 @@ def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
   getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
 
 /-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
-declarations with `sorryAx` generate the "declaration uses 'sorry'" warning. -/
+declarations with `sorryAx` generate the "declaration uses `sorry`" warning. -/
 register_builtin_option warn.sorry : Bool := {
   defValue := true
   descr    := "warn about uses of `sorry` in declarations added to the environment"
@@ -81,7 +81,7 @@ logs a warning if the declaration uses `sorry`.
 def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
   if warn.sorry.get (← getOptions) then
     if !(← MonadLog.hasErrors) && decl.hasSorry then
-      -- Find an actual sorry expression to use for 'sorry'.
+      -- Find an actual sorry expression to use for `sorry`.
       -- That way the user can hover over it to see its type and use "go to definition" if it is a labeled sorry.
       let findSorry : StateRefT (Array (Bool × MessageData)) MetaM Unit := decl.forEachSorryM fun s => do
         let s' ← addMessageContext s
@@ -91,10 +91,10 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
       -- These can appear without logged errors if `decl` is referring to declarations with elaboration errors;
       -- that's where a user should direct their focus.
       if let some (_, s) := sorries.find? (·.1) <|> sorries[0]? then
-        logWarning <| .tagged `hasSorry m!"declaration uses '{s}'"
+        logWarning <| .tagged `hasSorry m!"declaration uses `{s}`"
       else
         -- This case should not happen, but it ensures a warning will get logged no matter what.
-        logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+        logWarning <| .tagged `hasSorry m!"declaration uses `sorry`"
 
 builtin_initialize
   registerTraceClass `addDecl

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

@@ -159,7 +159,7 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme
   let some decl := env.find? 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/Compiler/CSimpAttr.lean

@@ -50,7 +50,7 @@ def add (declName : Name) (kind : AttributeKind) : CoreM Unit := do
   if let some entry ← isConstantReplacement? declName then
     ext.add entry kind
   else
-    throwError "invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported."
+    throwError "invalid `csimp` theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported."
 
 /--
 Tags compiler simplification theorems, which allow one value to be replaced by another equal value

src/Lean/Compiler/IR/Checker.lean

@@ -57,7 +57,7 @@ def markJP (j : JoinPointId) : M Unit :=
 def getDecl (c : Name) : M Decl := do
   let ctx ← read
   match findEnvDecl' (← getEnv) c ctx.decls with
-  | none   => throwCheckerError s!"depends on declaration '{c}', which has no executable code; consider marking definition as 'noncomputable'"
+  | none   => throwCheckerError s!"depends on declaration `{c}`, which has no executable code; consider marking definition as `noncomputable`"
   | some d => pure d
 
 def checkVar (x : VarId) : M Unit := do

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1067,7 +1067,7 @@ def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Na
   | IRType.uint16  => pure ("lean_ctor_set_uint16", ← LLVM.i16Type llvmctx)
   | IRType.uint32  => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
   | IRType.uint64  => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
-  | _              => throw s!"invalid type for 'lean_ctor_set': '{t}'"
+  | _              => throw s!"invalid type for `lean_ctor_set`: `{t}`"
   let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
@@ -1489,9 +1489,9 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   let d ← getDecl `main
   let xs ← match d with
    | .fdecl (xs := xs) .. => pure xs
-   | _ =>  throw "Function declaration expected for 'main'"
+   | _ =>  throw "Function declaration expected for `main`"
 
-  unless xs.size == 2 || xs.size == 1 do throw s!"Invalid main function, main expected to have '2' or '1' arguments, found '{xs.size}' arguments"
+  unless xs.size == 2 || xs.size == 1 do throw s!"Invalid main function, main expected to have `2` or `1` arguments, found `{xs.size}` arguments"
   let env ← getEnv
   let usesLeanAPI := usesModuleFrom env `Lean
   let mainTy ← LLVM.functionType (← LLVM.i64Type llvmctx)

src/Lean/Compiler/IR/ToIR.lean

@@ -252,7 +252,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
     | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>
       throwNamedError lean.dependsOnNoncomputable f!"`{name}` not supported by code generator; consider marking definition as `noncomputable`"
     | some (.recInfo ..) =>
-      throwError f!"code generator does not support recursor `{name}` yet, consider using 'match ... with' and/or structural recursion"
+      throwError f!"code generator does not support recursor `{name}` yet, consider using `match ... with` and/or structural recursion"
     | none => panic! "reference to unbound name"
   | .fvar fvarId args =>
     match (← getFVarValue fvarId) with

src/Lean/Compiler/LCNF/ToMono.lean

@@ -26,7 +26,7 @@ def Param.toMono (param : Param) : ToMonoM Param := do
   param.update (← toMonoType param.type)
 
 def throwNoncomputableError {α : Type} (declName : Name) : ToMonoM α :=
-  throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName declName}', which is 'noncomputable'"
+  throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as `noncomputable` because it depends on '{.ofConstName declName}', which is `noncomputable`"
 
 def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do
   if let some declName := (← get).noncomputableVars.get? fvarId then