chore: make use of string gaps (#480)

Std/Lean/CoreM.lean

@@ -45,5 +45,6 @@ def heartbeatsPercent : CoreM Nat := do
 /-- Log a message if it looks like we ran out of time. -/
 def reportOutOfHeartbeats (tac : Name) (stx : Syntax) (threshold : Nat := 90) : CoreM Unit := do
   if (← heartbeatsPercent) ≥ threshold then
-    logInfoAt stx (s!"`{tac}` stopped because it was running out of time.\n" ++
-      "You may get better results using `set_option maxHeartbeats 0`.")
+    logInfoAt stx s!"\
+      `{tac}` stopped because it was running out of time.\n\
+      You may get better results using `set_option maxHeartbeats 0`."

Std/Tactic/Case.lean

@@ -126,9 +126,9 @@ def findGoalOfPatt (gs : List MVarId)
       else
         let g ← renameInaccessibles g renameI
         return (g, [], gs)
-    throwError "No goals with tag {tag} unify with the term {patt?.getD (← `(_))}, {
-                ""}or too many names provided for renaming {
-                ""}inaccessible variables."
+    throwError "\
+      No goals with tag {tag} unify with the term {patt?.getD (← `(_))}, \
+      or too many names provided for renaming inaccessible variables."
 
 /-- Given a `casePattBody`, either give a synthetic hole or a tactic sequence
 (along with the syntax for the `=>`).
@@ -162,8 +162,9 @@ def evalCase (close : Bool) (stx : Syntax)
       let gs' ← run g <| withRef hole do
         let (val, gs') ← elabTermWithHoles hole (← getMainTarget) `case
         unless ← occursCheck g val do
-          throwError "'case' tactic failed, value{indentExpr val}\n{
-            ""}depends on the main goal metavariable '{Expr.mvar g}'"
+          throwError "\
+            'case' tactic failed, value{indentExpr val}\n\
+            depends on the main goal metavariable '{Expr.mvar g}'"
         g.assign val
         setGoals gs'
       acc := acc ++ gs'

Std/Tactic/Lint/Misc.lean

@@ -179,15 +179,15 @@ a higher universe level than `α`.
 @[std_linter] def checkUnivs : Linter where
   noErrorsFound :=
     "All declarations have good universe levels."
-  errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. " ++
-"This usually means that there is a `max u v` in the type where neither `u` nor `v` " ++
-"occur by themselves. Solution: Find the type (or type bundled with data) that has this " ++
-"universe argument and provide the universe level explicitly. If this happens in an implicit " ++
-"argument of the declaration, a better solution is to move this argument to a `variables` " ++
-"command (then it's not necessary to provide the universe level).
-It is possible that this linter gives a false positive on definitions where the value of the " ++
-"definition has the universes occur separately, and the definition will usually be used with " ++
-"explicit universe arguments. In this case, feel free to add `@[nolint checkUnivs]`."
+  errorsFound := "THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. \
+    This usually means that there is a `max u v` in the type where neither `u` nor `v` \
+    occur by themselves. Solution: Find the type (or type bundled with data) that has this \
+    universe argument and provide the universe level explicitly. If this happens in an implicit \
+    argument of the declaration, a better solution is to move this argument to a `variables` \
+    command (then it's not necessary to provide the universe level).\n\n\
+    It is possible that this linter gives a false positive on definitions where the value of the \
+    definition has the universes occur separately, and the definition will usually be used with \
+    explicit universe arguments. In this case, feel free to add `@[nolint checkUnivs]`."
   isFast := true
   test declName := do
     if ← isAutoDecl declName then return none
@@ -204,12 +204,12 @@ with rfl when elaboration results in a different term than the user intended. -/
 @[std_linter] def synTaut : Linter where
   noErrorsFound :=
     "No declarations are syntactic tautologies."
-  errorsFound := "THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. " ++
-"This usually means that they are of the form `∀ a b ... z, e₁ = e₂` where `e₁` and `e₂` are " ++
-"identical expressions. We call declarations of this form syntactic tautologies. " ++
-"Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving " ++
-"basic facts using `rfl`, when elaboration results in a different term than the user intended. " ++
-"You should check that the declaration really says what you think it does."
+  errorsFound := "THE FOLLOWING DECLARATIONS ARE SYNTACTIC TAUTOLOGIES. \
+    This usually means that they are of the form `∀ a b ... z, e₁ = e₂` where `e₁` and `e₂` are \
+    identical expressions. We call declarations of this form syntactic tautologies. \
+    Such lemmas are (mostly) useless and sometimes introduced unintentionally when proving \
+    basic facts using `rfl`, when elaboration results in a different term than the user intended. \
+    You should check that the declaration really says what you think it does."
   isFast := true
   test declName := do
     if ← isAutoDecl declName then return none
@@ -238,16 +238,16 @@ tag this as `@[std_linter]` so that it is not in the default linter set as it is
 uncommon problem. -/
 @[std_linter] def unusedHavesSuffices : Linter where
   noErrorsFound := "No declarations have unused term mode have statements."
-  errorsFound := "THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. " ++
-    "In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not " ++
-    "refer to `foo`. Such statements have no effect on the generated proof, and can just be " ++
-    "replaced by `bar`, in addition to being ineffectual, they may make unnecessary assumptions " ++
-    "in proofs appear as if they are used. " ++
-    "For `suffices` this is a term of the form `suffices h : foo, proof_of_goal, proof_of_foo`" ++
-    " where `proof_of_goal` does not refer to `foo`. " ++
-    "Such statements have no effect on the generated proof, and can just be replaced by " ++
-    "`proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions " ++
-    "in proofs appear as if they are used. "
+  errorsFound := "THE FOLLOWING DECLARATIONS HAVE INEFFECTUAL TERM MODE HAVE/SUFFICES BLOCKS. \
+    In the case of `have` this is a term of the form `have h := foo, bar` where `bar` does not \
+    refer to `foo`. Such statements have no effect on the generated proof, and can just be \
+    replaced by `bar`, in addition to being ineffectual, they may make unnecessary assumptions \
+    in proofs appear as if they are used. \
+    For `suffices` this is a term of the form `suffices h : foo, proof_of_goal, proof_of_foo` \
+    where `proof_of_goal` does not refer to `foo`. \
+    Such statements have no effect on the generated proof, and can just be replaced by \
+    `proof_of_goal`, in addition to being ineffectual, they may make unnecessary assumptions \
+    in proofs appear as if they are used."
   test declName := do
     if ← isAutoDecl declName then return none
     let info ← getConstInfo declName

Std/Tactic/NormCast/Ext.lean

@@ -89,15 +89,15 @@ def classifyType (ty : Expr) : MetaM Label :=
     else if rhsHeadCoes < lhsHeadCoes then do
       return Label.squash
     else do
-      throwError
-          ("norm_cast: badly shaped shaped squash lemma, " ++
-        "rhs must have fewer head coes than lhs{indentExpr ty}")
+      throwError "\
+        norm_cast: badly shaped shaped squash lemma, \
+        rhs must have fewer head coes than lhs{indentExpr ty}"
 
 /-- The `push_cast` simp attribute. -/
 initialize pushCastExt : SimpExtension ←
-  registerSimpAttr `push_cast <|
-    "The `push_cast` simp attribute uses `norm_cast` lemmas " ++
-    "to move casts toward the leaf nodes of the expression."
+  registerSimpAttr `push_cast "\
+    The `push_cast` simp attribute uses `norm_cast` lemmas \
+    to move casts toward the leaf nodes of the expression."
 
 /--  The `norm_cast` attribute stores three simp sets. -/
 structure NormCastExtension where

Std/Tactic/RCases.lean

@@ -712,9 +712,9 @@ elab (name := obtain) tk:"obtain"
     pat:(ppSpace rcasesPatMed)? ty:((" : " term)?) val:((" := " term,+)?) : tactic => do
   let pat ← liftM $ pat.mapM RCasesPatt.parse
   if val.raw.isNone then
-    if ty.raw.isNone then throwError
-        ("`obtain` requires either an expected type or a value.\n" ++
-        "usage: `obtain ⟨patt⟩? : type (:= val)?` or `obtain ⟨patt⟩? (: type)? := val`")
+    if ty.raw.isNone then throwError "\
+      `obtain` requires either an expected type or a value.\n\
+      usage: `obtain ⟨patt⟩? : type (:= val)?` or `obtain ⟨patt⟩? (: type)? := val`"
     let pat := pat.getD (RCasesPatt.one tk `this)
     let g ← getMainGoal
     g.withContext do replaceMainGoal (← RCases.obtainNone pat ty.raw[1] g)