From f1762c3debdbbb7cf409bd81b70e0a221d86e33c Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Wed, 6 Nov 2024 02:52:36 +0900
Subject: [PATCH] =?UTF-8?q?Array=20=E5=9E=8B=E3=82=92=E7=B4=B9=E4=BB=8B?=
 =?UTF-8?q?=E3=81=99=E3=82=8B=20Fixes=20#827?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Reference/Type/Array.lean | 73 +++++++++++++++++++++++++
 booksrc/SUMMARY.md                      |  1 +
 2 files changed, 74 insertions(+)
 create mode 100644 LeanByExample/Reference/Type/Array.lean

diff --git a/LeanByExample/Reference/Type/Array.lean b/LeanByExample/Reference/Type/Array.lean
new file mode 100644
index 0000000..9b1d4fa
--- /dev/null
+++ b/LeanByExample/Reference/Type/Array.lean
@@ -0,0 +1,73 @@
+/- # Array
+
+`Array α` は配列を表す型です。特定の型 `α : Type u` の要素を一直線に並べたものです。
+`#[a₁, ..., aₖ]` という記法で `Array α` の項を作ることができます。
+-/
+import Lean --#
+
+#check (#[1, 2, 3] : Array Nat)
+
+#check (#["hello", "world"] : Array String)
+
+/- ## 定義と実行時の性質
+
+`Array α` は次のように連結リスト `List α` のラッパーとして定義されているように見えます。-/
+--#--
+/--
+info: structure Array.{u} : Type u → Type u
+number of parameters: 1
+constructor:
+Array.mk : {α : Type u} → List α → Array α
+fields:
+toList : List α
+-/
+#guard_msgs in #print Array
+--#--
+
+namespace Hidden --#
+
+structure Array.{u} (α : Type u) : Type u where
+  toList : List α
+
+end Hidden --#
+/- しかしドキュメントコメントに以下のように書かれている通り、実行時には `List` とは大きく異なる動的配列(dynamic array)としての振る舞いを見せます。-/
+
+open Lean Elab Command in
+
+/-- ドキュメントコメントを取得して表示するコマンド -/
+elab "#doc " x:ident : command => do
+  let name ← liftCoreM do realizeGlobalConstNoOverload x
+  if let some s ← findDocString? (← getEnv) name then
+  logInfo m!"{s}"
+
+/--
+info: `Array α` is the type of [dynamic arrays](https://en.wikipedia.org/wiki/Dynamic_array)
+with elements from `α`. This type has special support in the runtime.
+
+An array has a size and a capacity; the size is `Array.size` but the capacity
+is not observable from Lean code. Arrays perform best when unshared; as long
+as they are used "linearly" all updates will be performed destructively on the
+array, so it has comparable performance to mutable arrays in imperative
+programming languages.
+
+From the point of view of proofs `Array α` is just a wrapper around `List α`.
+-/
+#guard_msgs in #doc Array
+
+/- `List` のラッパーとしての定義は、証明を行おうとしたときに参照されます。-/
+
+/- ## インデックスアクセス
+
+配列は [`GetElem`](#{root}/Reference/TypeClass/GetElem.md) のインスタンスであり、`i` 番目の要素を取得するために `a[i]` という記法が使用できます。
+-/
+
+#guard #[1, 2, 3][0] = 1
+
+#guard #[1, 2, 3][3]? = none
+
+/- ## 要素の追加
+
+`xs : Array α` に対して `Array.push` 関数で末尾に要素を追加できます。
+-/
+
+#guard #[1, 2, 3].push 4 = #[1, 2, 3, 4]
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 63a4aa1..f0b516b 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -93,6 +93,7 @@
   - [ToString: 文字列に変換](./Reference/TypeClass/ToString.md)
 
 - [型](./Reference/Type/README.md)
+  - [Array: 配列](./Reference/Type/Array.md)
   - [Bool: 真偽値](./Reference/Type/Bool.md)
   - [Char: Unicode 文字](./Reference/Type/Char.md)
   - [Float: 浮動小数点数](./Reference/Type/Float.md)