`String.take` / `drop` と `String.Slice` による文字列スライス例を追加したい

## 概要 最近の Lean 公式 Zulip に `Basic string slicing` という話題があり、Lean で「文字列の一部を取り出したい」ときに、まず何を使えばよいかを整理した短い実例があると Lean by Example に追加価値があると感じました。 特に Lean では、`String.take` / `drop` / `takeEnd` / `dropEnd` が**すぐに `String` を返すのではなく `String.Slice` を返す**、という点が初見では分かりづらいです。必要になったときだけ `.copy` して `String` に戻す、という流れは標準ライブラリ的には自然ですが、入門者はかなり引っかかりやすいポイントだと思います。 ## 投稿元 - Zulip: [Basic string slicing](https://leanprover-community.github.io/archive/stream/270676-lean4/topic/Basic.20string.20slicing.html) ## 重複確認 確認した既存ページ: - `LeanByExample/Type/String.lean` - 文字列の基本として `String.ofList` / `toList`、連結、長さ、文字列補間は扱っている - ただし `take` / `drop` / `takeEnd` / `dropEnd` / `String.Slice` / `dropPrefix?` の説明は見当たらなかった 確認した検索: - GitHub code search: `"String.Slice"` in `lean-ja/lean-by-example` → 0件 - GitHub code search: `"takeEnd"` / `"dropEnd"` / `"dropPrefix?"` in `lean-ja/lean-by-example` → relevant result 0件 - GitHub issue search: `String.Slice take drop takeEnd dropEnd extract` → 0件 ## 追加候補のコード例 ```lean -- `take` / `drop` は `String` ではなく `String.Slice` を返す #guard "red green blue".take 3 = "red".toSlice #guard "red green blue".drop 4 = "green blue".toSlice #guard "red green blue".takeEnd 4 = "blue".toSlice #guard "red green blue".dropEnd 5 = "red green".toSlice -- 必要になったときだけ `.copy` して `String` にする #guard ("red green blue".drop 4).take 5 |>.copy = "green" -- 文字数ベースで扱われるので、Unicode 文字列にもそのまま使える #guard "مرحبا بالعالم".take 5 = "مرحبا".toSlice -- 既知の接頭辞を落としたいなら `dropPrefix?` も便利 #guard "red green blue".dropPrefix? "red " = some "green blue".toSlice #guard "green blue".dropPrefix? "red " = none ``` ## この例の何が面白いか - 「部分文字列を取りたい」という初歩的な要求に対して、Lean ではまず `String.Slice` を返す API を使う、という設計が分かる - `take` / `drop` が**文字数（Unicode code point）単位**で動くことを短い例で示せる - `dropPrefix?` のような派生 API まで見せると、「単なる添字スライス」以外の実用的な文字列処理へ自然につなげられる ## コードの読み方 - `"red green blue".take 3` は先頭 3 文字を表す `String.Slice` を返す - `"red green blue".drop 4` は先頭 4 文字を落とした残りを `String.Slice` で返す - `("red green blue".drop 4).take 5` と続けると、まず `"green blue"` に相当するスライスを作り、そこからさらに先頭 5 文字を切り出している - `.copy` を呼ぶまで新しい `String` を確保しない、というのが `Slice` を使う利点 - `dropPrefix?` は「この接頭辞があれば落とす、なければ失敗」という `Option` ベースの API になっている ## Lean by Example に追加する価値 - 文字列処理の入口として需要が高いのに、Lean の `String` API は `Slice` を経由する点が直感に反する - `String` と `String.Slice` の役割分担を入門段階で一度見せておくと、以後の文字列 API の読み方がかなり楽になる - 既存の `Type/String.lean` は「文字列とは何か」の導入としては十分だが、「文字列の一部を取り出す」具体操作はまだ空いている ## 前提・曖昧な点 - 今回の自動化環境では Zulip 個別スレッド本文を安定して取得できず、`Basic string slicing` というトピック名から「Lean での基本的な文字列スライス API を紹介する話題」と解釈して候補化しています - そのため上のコード例は Zulip の投稿本文の転載ではなく、**現在の Lean コア API と公式ドキュメントに基づく再構成例**です - 実装時には、必要なら `String.extract` の legacy API も比較対象として補足してよいと思いますが、入門向けにはまず `take` / `drop` と `String.Slice` を主役にした方が分かりやすそうです