diff --git a/LeanByExample/Type/String.lean b/LeanByExample/Type/String.lean index 09a647d5..b9bd5016 100644 --- a/LeanByExample/Type/String.lean +++ b/LeanByExample/Type/String.lean @@ -1,6 +1,6 @@ /- # String -`String` は文字列を表す型です。次のように、文字を表す型 [`Char`](./Char.md) のリストとして定義されています。 +`String` は文字列を表す型です。次のように、文字を表す型 [`Char`](#{root}/Type/Char.md) のリストとして定義されています。 -/ import Lean --# --#-- @@ -45,7 +45,7 @@ end Hidden --# 1. 文字列を `List Char` に変換する 2. `List.length` を使って長さを求める -という手順になるかと思います。`n` 個の要素を持つ `xs : List α` に対して長さを求めようとすると、先頭から順に要素をたぐっていくので `Ω(n)` 時間がかかります。したがって `String.length` は長い文字列に対しては遅くなりそうなものですが、コンパイラによって実装がオーバーライドされているため実際には `O(1)` 時間で実行できます。 +という手順になるかと思います。`n` 個の要素を持つ `xs : List α` に対して長さを求めようとすると、先頭から順に要素をたぐっていくので `n` に比例する時間がかかります。したがって `String.length` は長い文字列に対しては遅くなりそうなものですが、コンパイラによって実装がオーバーライドされているため、実際には `n` が大きくても高速に実行できます。 このあたりの背景はドキュメントコメントに書かれています。 -/