表記を微修正

dependent_type_theory.md

@@ -221,8 +221,8 @@ Leanでは、キーワード ``fun`` (あるいは ``λ``) を使うと、式か
 -- λ (<入力引数の名前> : <入力引数の型名>) => <関数の出力を定義する式>
 #check fun (x : Nat) => x + 5   -- Nat → Nat
 #check λ (x : Nat) => x + 5     -- `λ` と `fun` は同じ意味
-#check fun x => x + 5           -- `x`は`Nat`型だと推論される
-#check λ x => x + 5             -- `x`は`Nat`型だと推論される
+#check fun x => x + 5           -- `x` は `Nat` 型だと推論される
+#check λ x => x + 5             -- `x` は `Nat` 型だと推論される
 ```
 
 要求されたパラメータを通すことにより、ラムダ関数を評価することができる。
@@ -711,7 +711,7 @@ def cons (α : Type) (a : α) (as : List α) : List α :=
 #check @List.append  -- {α : Type u_1} → List α → List α → List α
 ```
 
-``β`` が ``α`` に依存できるようにすることで依存関数型 ``(a : α) → β a`` が関数型 ``α → β`` を一般化するのと同様に、依存積型 ``(a : α) × β a`` は直積型 ``α × β`` を一般化する。依存積型は ``β`` が ``a`` に依存することを可能にする。依存積型は*sigma*(Σ)型とも呼ばれ、``(a : α) × β a`` は ``Σ a : α, β a`` とも書かれる。Leanにおいて、``⟨a, b⟩`` あるいは ``Sigma.mk a b`` と書くと依存ペアを作ることができる。`⟨` は "\langle" または "\<" と打つと入力でき、`⟩` は "\rangle" または "\>" と打つと入力できる。
+``β`` が ``α`` に依存できるようにすることで依存関数型 ``(a : α) → β a`` が関数型 ``α → β`` を一般化するのと同様に、依存積型 ``(a : α) × β a`` は直積型 ``α × β`` を一般化する。依存積型は ``β`` が ``a`` に依存することを可能にする。依存積型は*sigma*(Σ)型とも呼ばれ、``(a : α) × β a`` は ``Σ a : α, β a`` とも書かれる。Leanにおいて、``⟨a, b⟩`` あるいは ``Sigma.mk a b`` と書くと依存ペアを作ることができる。`⟨` は ``\langle`` または ``\<`` と打つと入力でき、`⟩` は ``\rangle`` または ``\>`` と打つと入力できる。
 
 ```lean
 universe u v