Merge pull request #348 from lean-ja/Seasawher/issue347

対話的コマンドと構文をひとつのカテゴリにまとめる

Examples/DiagnosticCommand/Check.lean → Examples/Command/Check.lean

@@ -1,97 +1,97 @@
-/- # \#check
-
-`#check` コマンドは，項の型を表示します．Lean ではすべての項に型があるので，どんな項にも使えます．`#check term` というコマンドで，`term` の型を表示します．逆に `term` の型が `T` であることを確かめるには `example` コマンドを使用して `example : T := term` とします．
-
-## 基本的な項の型 -/
-
--- 文字
-#check 'a'
-
--- 文字列
-#check "Hello"
-
--- 自然数
-#check 1
-
--- 浮動小数点数
-#check 1.0
-
--- 整数
-#check -2
-
--- `1` はそのままだと自然数扱いになるが，整数にキャストできる
-#check (1 : Int)
-
--- 自然数のリスト
-#check [1, 2, 3]
-
--- 自然数の配列
-#check #[1, 2, 3]
-
--- 関数
-#check fun x ↦ x + 42
-
--- Bool, 真偽値
-#check true
-
--- 命題
-#check True
-
-/-! ## 型の型
-「すべての」項には型があるので，型も型を持ちます．
--/
--- 宇宙変数を宣言する
-universe u
-
-#check (Prop : Type)
-
--- Lean では `List` は Type を受け取って，Type を返す関数.
-#check (List : (α : Type u) → Type u)
-
--- 配列も同じ．型を型に変換する関数．
-#check (Array : (α : Type u) → Type u)
-
--- `Type` 自身も型を持っており…
-#check (Type : Type 1)
-
-#check (Type 1 : Type 2)
-
--- この調子で限りなく続く
-#check (Type u : Type (u + 1))
-
-/-! ## 命題と証明
-Lean では命題やその証明にも型があります．命題の型は `Prop` で，命題の項が証明になっています．逆に言えば，Lean ではある命題 `P : Prop` を証明するということは，`P` という型を持つ項 `proof : P` を構成することと同じです．
--/
-
-#check (1 + 1 = 2 : Prop)
-
--- `1 + 1 = 2` の証明 `two_eq_add_one` を構成
-theorem two_eq_add_one : 2 = 1 + 1 := by rfl
-
--- 証明の型が命題になっている
-#check (two_eq_add_one : 2 = 1 + 1)
-
-/-! ## 型としての True/False
-`True` は型としては一点集合であり，
-`False` は型としては空集合です．
--/
-
--- `trivial : True` は `True` 型を持つ項
-#check trivial
-
-/-! ## 関数としての証明
-命題 `P → Q` の証明は，`P → Q` という型を持つ項です．
-つまり，`P` の証明 `h : P` に対して `Q` の証明を返す関数です．
--/
-
-theorem tautology : True -> True := fun a ↦ a
-
--- 暗黙の変数を明示的にするために `@` を付けた.
--- `tautology : True → True` と出力されるので，
--- `tautology` は `True → True` という関数であることがわかる
-#check (@tautology : True → True)
-
--- 実際に `trivial : True` を「代入」すると
--- `tautology trivial : True` となり，
--- 確かに `True` 型の項が得られていることがわかる．
-#check (tautology trivial : True)
+/- # \#check
+
+`#check` コマンドは，項の型を表示します．Lean ではすべての項に型があるので，どんな項にも使えます．`#check term` というコマンドで，`term` の型を表示します．逆に `term` の型が `T` であることを確かめるには `example` コマンドを使用して `example : T := term` とします．
+
+## 基本的な項の型 -/
+
+-- 文字
+#check 'a'
+
+-- 文字列
+#check "Hello"
+
+-- 自然数
+#check 1
+
+-- 浮動小数点数
+#check 1.0
+
+-- 整数
+#check -2
+
+-- `1` はそのままだと自然数扱いになるが，整数にキャストできる
+#check (1 : Int)
+
+-- 自然数のリスト
+#check [1, 2, 3]
+
+-- 自然数の配列
+#check #[1, 2, 3]
+
+-- 関数
+#check fun x ↦ x + 42
+
+-- Bool, 真偽値
+#check true
+
+-- 命題
+#check True
+
+/-! ## 型の型
+「すべての」項には型があるので，型も型を持ちます．
+-/
+-- 宇宙変数を宣言する
+universe u
+
+#check (Prop : Type)
+
+-- Lean では `List` は Type を受け取って，Type を返す関数.
+#check (List : (α : Type u) → Type u)
+
+-- 配列も同じ．型を型に変換する関数．
+#check (Array : (α : Type u) → Type u)
+
+-- `Type` 自身も型を持っており…
+#check (Type : Type 1)
+
+#check (Type 1 : Type 2)
+
+-- この調子で限りなく続く
+#check (Type u : Type (u + 1))
+
+/-! ## 命題と証明
+Lean では命題やその証明にも型があります．命題の型は `Prop` で，命題の項が証明になっています．逆に言えば，Lean ではある命題 `P : Prop` を証明するということは，`P` という型を持つ項 `proof : P` を構成することと同じです．
+-/
+
+#check (1 + 1 = 2 : Prop)
+
+-- `1 + 1 = 2` の証明 `two_eq_add_one` を構成
+theorem two_eq_add_one : 2 = 1 + 1 := by rfl
+
+-- 証明の型が命題になっている
+#check (two_eq_add_one : 2 = 1 + 1)
+
+/-! ## 型としての True/False
+`True` は型としては一点集合であり，
+`False` は型としては空集合です．
+-/
+
+-- `trivial : True` は `True` 型を持つ項
+#check trivial
+
+/-! ## 関数としての証明
+命題 `P → Q` の証明は，`P → Q` という型を持つ項です．
+つまり，`P` の証明 `h : P` に対して `Q` の証明を返す関数です．
+-/
+
+theorem tautology : True -> True := fun a ↦ a
+
+-- 暗黙の変数を明示的にするために `@` を付けた.
+-- `tautology : True → True` と出力されるので，
+-- `tautology` は `True → True` という関数であることがわかる
+#check (@tautology : True → True)
+
+-- 実際に `trivial : True` を「代入」すると
+-- `tautology trivial : True` となり，
+-- 確かに `True` 型の項が得られていることがわかる．
+#check (tautology trivial : True)

Examples/Syntax/Class.lean → Examples/Command/Class.lean

@@ -1,78 +1,78 @@
-/-
-# class
-`class` は型クラスを定義するための構文です．型クラスを用いると，複数の型に対して定義され，型ごとに異なる実装を持つような関数を定義することができます．例えば「和を取る操作」のような，`Nat` や `Int` や `Rat` など複数の型に対して同じ名前で定義したい関数を作りたいとき，型クラスが適しています．
--/
-
-/-- 証明なしのバージョンのモノイド -/
-class Monoid (α : Type) where
-  /-- 単位元 -/
-  e : α
-
-  /-- 二項演算 -/
-  op : α → α → α
-
-/-- 自然数はモノイド -/
-instance : Monoid Nat where
-  -- ゼロを単位元とする
-  e := 0
-
-  -- 加算を二項演算とする
-  op := Nat.add
-
-/-- 連結リストはモノイド -/
-instance {α : Type} : Monoid (List α) where
-  -- 空リストを単位元とする
-  e := []
-
-  -- リストの連結を二項演算とする
-  op := List.append
-
--- `Nat` に対してモノイドの演算が使える
-#guard Monoid.op 0 0 = 0
-
--- `List Nat` に対してモノイドの演算が使える
-#guard Monoid.op [1] [2, 3] = [1, 2, 3]
-
--- `Nat` に対して単位元を取得する関数が使える
-#guard (Monoid.e : Nat) = 0
-
--- `List Int` に対しても単位元を取得する関数が使える
-#guard (Monoid.e : List Int) = []
-
-/- ## 舞台裏
-
-### 構造体による型クラスの模倣
-型クラスが行っていることを `class` を使わずにDIYしてみると，型クラスの理解が深まるでしょう．`class` として上で定義したものを，もう一度 `structure` として定義してみます．-/
-
-/-- 構造体でモノイドクラスを真似たもの -/
-structure Monoid' (α : Type) where
-  e : α
-  op : α → α → α
-
-/-- 自然数がモノイドのインスタンスであるという主張を再現したもの -/
-def instMonoid'Nat : Monoid' Nat where
-  e := 0
-  op := Nat.add
-
-/- このとき構造体 `Monoid'` のフィールド `Monoid'.e` は，「`Monoid'` の項に対して `α` の要素を返す」関数なので，次のような型を持ちます．-/
-
-/-- info: Monoid'.e {α : Type} (self : Monoid' α) : α -/
-#guard_msgs in #check Monoid'.e
-
-/- `self : Monoid' α` が暗黙の引数ではなく明示的な引数なので, 型クラスのように書くことはできません．-/
-
-#check_failure (Monoid'.e : Nat)
-
-/- しかし，インスタンスを引数として渡せば，型クラスのように `Nat` の要素を取り出すことができます．-/
-
-#check (Monoid'.e instMonoid'Nat : Nat)
-
-/- 構造体による模倣と本物の型クラスの違いがどこにあるのかおわかりいただけたでしょうか．最大の違いは，引数の `instMonoid'Nat` が省略できるかどうかです．-/
-
-/- ### インスタンス暗黙引数と型クラス解決
-ここで(本物の)型クラスにおける単位元関数 `e` の型を調べてみると, `self : Monoid' α` が角括弧 `[ .. ]` で囲われていることがわかります．-/
-
-/-- info: Monoid.e {α : Type} [self : Monoid α] : α -/
-#guard_msgs in #check Monoid.e
-
-/- これは**インスタンス暗黙引数**と呼ばれるもので，この場合 Lean に対して `Monoid' α` 型の項を自動的に合成するよう指示することを意味します．また，型クラスのインスタンス暗黙引数を自動的に合成する手続きのことを，**型クラス解決**と呼びます．-/
+/-
+# class
+`class` は型クラスを定義するための構文です．型クラスを用いると，複数の型に対して定義され，型ごとに異なる実装を持つような関数を定義することができます．例えば「和を取る操作」のような，`Nat` や `Int` や `Rat` など複数の型に対して同じ名前で定義したい関数を作りたいとき，型クラスが適しています．
+-/
+
+/-- 証明なしのバージョンのモノイド -/
+class Monoid (α : Type) where
+  /-- 単位元 -/
+  e : α
+
+  /-- 二項演算 -/
+  op : α → α → α
+
+/-- 自然数はモノイド -/
+instance : Monoid Nat where
+  -- ゼロを単位元とする
+  e := 0
+
+  -- 加算を二項演算とする
+  op := Nat.add
+
+/-- 連結リストはモノイド -/
+instance {α : Type} : Monoid (List α) where
+  -- 空リストを単位元とする
+  e := []
+
+  -- リストの連結を二項演算とする
+  op := List.append
+
+-- `Nat` に対してモノイドの演算が使える
+#guard Monoid.op 0 0 = 0
+
+-- `List Nat` に対してモノイドの演算が使える
+#guard Monoid.op [1] [2, 3] = [1, 2, 3]
+
+-- `Nat` に対して単位元を取得する関数が使える
+#guard (Monoid.e : Nat) = 0
+
+-- `List Int` に対しても単位元を取得する関数が使える
+#guard (Monoid.e : List Int) = []
+
+/- ## 舞台裏
+
+### 構造体による型クラスの模倣
+型クラスが行っていることを `class` を使わずにDIYしてみると，型クラスの理解が深まるでしょう．`class` として上で定義したものを，もう一度 `structure` として定義してみます．-/
+
+/-- 構造体でモノイドクラスを真似たもの -/
+structure Monoid' (α : Type) where
+  e : α
+  op : α → α → α
+
+/-- 自然数がモノイドのインスタンスであるという主張を再現したもの -/
+def instMonoid'Nat : Monoid' Nat where
+  e := 0
+  op := Nat.add
+
+/- このとき構造体 `Monoid'` のフィールド `Monoid'.e` は，「`Monoid'` の項に対して `α` の要素を返す」関数なので，次のような型を持ちます．-/
+
+/-- info: Monoid'.e {α : Type} (self : Monoid' α) : α -/
+#guard_msgs in #check Monoid'.e
+
+/- `self : Monoid' α` が暗黙の引数ではなく明示的な引数なので, 型クラスのように書くことはできません．-/
+
+#check_failure (Monoid'.e : Nat)
+
+/- しかし，インスタンスを引数として渡せば，型クラスのように `Nat` の要素を取り出すことができます．-/
+
+#check (Monoid'.e instMonoid'Nat : Nat)
+
+/- 構造体による模倣と本物の型クラスの違いがどこにあるのかおわかりいただけたでしょうか．最大の違いは，引数の `instMonoid'Nat` が省略できるかどうかです．-/
+
+/- ### インスタンス暗黙引数と型クラス解決
+ここで(本物の)型クラスにおける単位元関数 `e` の型を調べてみると, `self : Monoid' α` が角括弧 `[ .. ]` で囲われていることがわかります．-/
+
+/-- info: Monoid.e {α : Type} [self : Monoid α] : α -/
+#guard_msgs in #check Monoid.e
+
+/- これは**インスタンス暗黙引数**と呼ばれるもので，この場合 Lean に対して `Monoid' α` 型の項を自動的に合成するよう指示することを意味します．また，型クラスのインスタンス暗黙引数を自動的に合成する手続きのことを，**型クラス解決**と呼びます．-/