StringGaps の例（TermElab の実装例、elab コマンド使用例）

import Lean.Parser.Extension
import Lean.Elab.Term

/-!
## Scala-style `stripMargin` 風の字下げ除去 + 文字列リテラル展開

### 目的
インデント付きの複数行文字列を、先頭行以外の各行の先頭に `|` を置くことで
共通インデントを落とし（字下げ除去 / dedent）、その結果を生の文字列リテラルとして
式に埋め込めるようにします。Scala の `stripMargin` に近い挙動です。

### 実装のあらまし
1. `String.dedent : String → Option String`
  - 文字列を改行で分割し、**各行の左側空白を一旦落として**から、
    先頭行以外のすべての行が `|` で始まるかを検査します。
  - 条件を満たせば `|` を 1 文字落として行を再構成し、`some ...` を返します。
  - 条件を満たさない場合は `none` を返します（= 構文として不正）。
2. カスタムの term elaborator `d!`
  - `"d!" s:str : term` という形で、直後に **通常の文字列リテラル**が来ることを要求します。
  - `isStrLit?` で生文字列を取り出し、`String.dedent` に通します。
  - `none` のときは `throwIllFormedSyntax` で構文エラーにします。
  - 成功したら `Lean.mkStrLit` で **ふつうの文字列リテラル式**に戻して返します。
-/

/-- `stripMargin` 風の字下げ除去を行う関数。

入力文字列 `s` を改行で分割し、**各行をいったん `trimLeft` した上で**判定します。
- 先頭行はそのまま採用します。
- 2 行目以降の各行は、**必ず** `|` で始まる必要があります。満たさなければ `none`。
- 条件を満たすとき、2 行目以降の行では先頭の `|` を 1 文字落として再結合します。

返り値は成功時に `some 結果文字列`、失敗時に `none`。
-/
def String.dedent (s : String) : Option String :=
  let parts := s.split (· == '\n') |>.map String.trimLeft
  match parts with
  | [] => ""
  | [p] => p
  | p₀ :: parts =>
    if !parts.all (·.startsWith "|") then
      none
    else
      p₀ ++ "\n" ++ String.intercalate "\n" (parts.map fun p => p.drop 1)

/-- `d!"..."` という新しい**項**の構文を導入する elaborator。

- 引数は**通常の**文字列リテラルでなければならない（`isStrLit?` で検査）。
- `String.dedent` に通して `none` なら構文不正としてエラー。
- 成功したら `Lean.mkStrLit` で**普通の文字列リテラル式**を構築して返す。
-/
elab "d!" s:str : term => do
  let some s := s.raw.isStrLit? | Lean.Elab.throwIllFormedSyntax
  let some s := String.dedent s | Lean.Elab.throwIllFormedSyntax
  pure $ Lean.mkStrLit s

/-- info: "this is line 1\n  line 2, indented\nline 3" -/
#guard_msgs in
#eval d!"this is \
          line 1
        |  line 2, indented
        |line 3"

Start by reviewing the issue's String.dedent implementation and the d! term elaborator example, then inspect how examples are organized in the repository. Confirm where this StringGaps example belongs and what documentation or runnable example is expected before making changes.