「match 文」や「match 構文」などの訳語を「match 式」に統一 (#13)

induction_and_recursion.md

@@ -1161,7 +1161,7 @@ def foo (n : Nat) (b c : Bool) :=
 example : foo 7 true false = 9 := rfl
 ```
 
-Leanは、システムの全ての部分で、パターンマッチングを実装するために内部で ``match`` 構文を使用する。したがって、以下の4つの定義は全て同じ効果を持つ。
+Leanは、システムの全ての部分で、パターンマッチングを実装するために内部で ``match`` 式を使用する。したがって、以下の4つの定義は全て同じ効果を持つ。
 
 ```lean
 def bar₁ : Nat × Nat → Nat

inductive_types.md

@@ -72,7 +72,7 @@ inductive Weekday where
 
 ``sunday``、``monday``、...、``saturday`` は ``Weekday`` の互いに異なる項であり、それ以外に互いに異なる項はないと考えてほしい。除去則 ``Weekday.rec`` は 型 ``Weekday`` とそのコンストラクタを用いて定義されている。除去則は*recursor*(再帰子)とも呼ばれ、この型を*inductive*(帰納的)にしている: 除去則は、各コンストラクタに対応する値を割り当てることで、``Weekday`` 上の関数を定義することを可能にしている。直感的には、帰納型の項は各コンストラクタによって網羅的に生成され、帰納型はコンストラクタが構築する項以外の項を持たないということである。
 
-``Weekday`` から自然数への関数を定義するには、``match`` 文を使うことができる:
+``Weekday`` から自然数への関数を定義するには、``match`` 式を使うことができる:
 
 ```lean
 # inductive Weekday where
@@ -1074,7 +1074,7 @@ example (x : Nat) {y : Nat} (h : y > 0) : x % y < y := by
       assumption
 ```
 
-タクティク証明の中で ``match`` 記法を使うこともできる:
+タクティク証明の中で ``match`` を使うこともできる:
 
 ```lean
 example : p ∨ q → q ∨ p := by

quantifiers_and_equality.md

@@ -511,7 +511,7 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
   | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩
 ```
 
-``match`` 式はLeanの関数定義システムの一部であり、複雑な関数を定義する便利で表現力豊かな方法を提供する。再びカリー=ハワード同型により、この関数定義方法 ``match`` を証明の記述にも応用させることができる。``match`` 文は存在量化された主張を ``w`` と ``hw`` に「分解」する。これらは命題の証明記述内で使うことができる。より明確にするために、マッチで分解されてできた要素に型の注釈を付けることができる:
+``match`` 式はLeanの関数定義システムの一部であり、複雑な関数を定義する便利で表現力豊かな方法を提供する。再びカリー=ハワード同型により、この関数定義方法 ``match`` を証明の記述にも応用させることができる。``match`` 式は存在量化された主張を ``w`` と ``hw`` に「分解」する。これらは命題の証明記述内で使うことができる。より明確にするために、マッチで分解されてできた要素に型の注釈を付けることができる:
 
 ```lean
 # variable (α : Type) (p q : α → Prop)
@@ -520,7 +520,7 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
   | ⟨(w : α), (hw : p w ∧ q w)⟩ => ⟨w, hw.right, hw.left⟩
 ```
 
-match文を使って、存在量化子と連言を同時に分解することもできる:
+match 式を使って、存在量化子と連言を同時に分解することもできる:
 
 ```lean
 # variable (α : Type) (p q : α → Prop)
@@ -538,7 +538,7 @@ example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
   ⟨w, hqw, hpw⟩
 ```
 
-これは、基本的に上記の ``match`` 構文の代替表記に過ぎない。Leanでは、``fun`` キーワードの中で暗黙の ``match`` を使うこともできる:
+これは、基本的に上記の ``match`` 式の代替表記に過ぎない。Leanでは、``fun`` キーワードの中で暗黙の ``match`` を使うこともできる:
 
 ```lean
 # variable (α : Type) (p q : α → Prop)
@@ -573,7 +573,7 @@ theorem even_plus_even2 : ∀ a b : Nat, is_even a → is_even b → is_even (a
     ⟨(w1 + w2 : Nat), (hw3 : a + b = 2 * (w1 + w2))⟩
 ```
 
-マッチ文、匿名コンストラクタ、``rewrite`` タクティク……、この章で説明した様々な小道具を使ってこの証明を簡潔に書くと次のようになる:
+マッチ式、匿名コンストラクタ、``rewrite`` タクティク……、この章で説明した様々な小道具を使ってこの証明を簡潔に書くと次のようになる:
 
 ```lean
 # def is_even (a : Nat) := ∃ b, a = 2 * b