句読点が統一されていないミスを修正

functional-programming-lean/src/getting-to-know/evaluating.md

@@ -69,7 +69,7 @@ arguments, Lean simply writes the function next to its
 arguments (e.g. `f x`). Function application is one of the most common operations,
 so it pays to keep it concise. Rather than writing -->
 
-通常の数学的表記法でも, 大半のプログラミング言語でも, 関数をその引数に適用する際には括弧を使います（例：`f(x)`）が、Lean は単に関数をその引数の横に書きます (例：`f x`). 関数の使用は最も一般的な操作のひとつであるため, 簡潔であることが重要なのです．`{{#example_out Examples/Intro.lean stringAppendHello}}` を計算するには，
+通常の数学的表記法でも, 大半のプログラミング言語でも, 関数をその引数に適用する際には括弧を使います（例：`f(x)`）が, Lean は単に関数をその引数の横に書きます (例：`f x`). 関数の使用は最も一般的な操作のひとつであるため, 簡潔であることが重要なのです．`{{#example_out Examples/Intro.lean stringAppendHello}}` を計算するには，
 
 ```lean
 #eval String.append("Hello, ", "Lean!")
@@ -117,7 +117,7 @@ Because Lean is an expression-oriented functional language, there are no conditi
 They are written using `if`, `then`, and `else`. For
 instance, -->
 
-命令形言語には, しばしば2種類の条件分岐があります：Bool 値に基づいてどの命令を実行するかを決定する条件**文**と，Bool 値に基づいて2つの式のうちどちらを評価するかを決定する条件**式**です．たとえば C や C++ では、条件文は `if` と `else` を使って書かれ，条件式は三項演算子 `?` `:` を使って書かれます．Python では，条件文は `if` で始まりますが，条件式は `if` を真ん中に置きます．Lean はというと式指向の関数型言語ですから，条件文はありません．条件式のみです．条件式は `if`, `then`, `else` を使って書かれます．例えば，
+命令形言語には, しばしば2種類の条件分岐があります：Bool 値に基づいてどの命令を実行するかを決定する条件**文**と，Bool 値に基づいて2つの式のうちどちらを評価するかを決定する条件**式**です．たとえば C や C++ では, 条件文は `if` と `else` を使って書かれ，条件式は三項演算子 `?` `:` を使って書かれます．Python では，条件文は `if` で始まりますが，条件式は `if` を真ん中に置きます．Lean はというと式指向の関数型言語ですから，条件文はありません．条件式のみです．条件式は `if`, `then`, `else` を使って書かれます．例えば，
 
 ``` Lean
 {{#example_eval Examples/Intro.lean stringAppend 0}}

functional-programming-lean/src/getting-to-know/functions-and-definitions.md

@@ -3,7 +3,7 @@
 
 <!-- In Lean, definitions are introduced using the `def` keyword. For instance, to define the name `{{#example_in Examples/Intro.lean helloNameVal}}` to refer to the string `{{#example_out Examples/Intro.lean helloNameVal}}`, write: -->
 
-Lean では，定義は `def` というキーワードを使って導入されます．例えば, 文字列 `{{#example_out Examples/Intro.lean helloNameVal}}` を指す名前として `{{#example_in Examples/Intro.lean helloNameVal}}` を定義するには、こう書きます：
+Lean では，定義は `def` というキーワードを使って導入されます．例えば, 文字列 `{{#example_out Examples/Intro.lean helloNameVal}}` を指す名前として `{{#example_in Examples/Intro.lean helloNameVal}}` を定義するには, こう書きます：
 
 ```lean
 {{#example_decl Examples/Intro.lean hello}}
@@ -74,7 +74,7 @@ Lean で関数を定義するには様々な方法があります．最もシン
 
 <!-- Just as functions are applied to multiple arguments by writing spaces between each argument, functions that accept multiple arguments are defined with spaces between the arguments' names and types. The function `maximum`, whose result is equal to the greatest of its two arguments, takes two `Nat` arguments `n` and `k` and returns a `Nat`. -->
 
-関数が各引数の間にスペースを書くことで複数の引数に適用されるように, 複数の引数を受け付ける関数は, 引数の名前と型の間にスペースを入れることで定義されます．関数 `maximum` は，2つの引数の最大値を返すもので，2つの `Nat` 型引数 `n` と `k` を取り、`Nat` を返します．
+関数が各引数の間にスペースを書くことで複数の引数に適用されるように, 複数の引数を受け付ける関数は, 引数の名前と型の間にスペースを入れることで定義されます．関数 `maximum` は，2つの引数の最大値を返すもので，2つの `Nat` 型引数 `n` と `k` を取り, `Nat` を返します．
 
 ```lean
 {{#example_decl Examples/Intro.lean maximum}}

functional-programming-lean/src/getting-to-know/types.md

@@ -77,7 +77,7 @@ provide it directly: -->
 <!-- To check the type of an expression without evaluating it, use `#check`
 instead of `#eval`. For instance: -->
 
-式を評価せずに型を確かめるには、`#eval` の代わりに `#check` を使います．例えば
+式を評価せずに型を確かめるには, `#eval` の代わりに `#check` を使います．例えば
 
 ```lean
 {{#example_in Examples/Intro.lean oneMinusTwoIntType}}

functional-programming-lean/src/introduction.md

@@ -21,7 +21,7 @@ Familiarity with functional languages such as Haskell, OCaml, or F# is not requi
 On the other hand, this book does assume knowledge of concepts like loops, functions, and data structures that are common to most programming languages.
 While this book is intended to be a good first book on functional programming, it is not a good first book on programming in general. -->
 
-本書は，Lean を学びたいが，必ずしも関数型言語を使ったことがないプログラマを対象としています．Haskell、OCaml、F# などの関数型言語に精通していることは必須ではありません．一方，本書はループ・関数・データ構造など，ほとんどのプログラミング言語に共通する概念の知識を前提としています．本書は関数型プログラミングの最初の一冊としては好適ですが，プログラミング全般の最初の一冊としては不適切です．
+本書は，Lean を学びたいが，必ずしも関数型言語を使ったことがないプログラマを対象としています．Haskell, OCaml, F# などの関数型言語に精通していることは必須ではありません．一方，本書はループ・関数・データ構造など，ほとんどのプログラミング言語に共通する概念の知識を前提としています．本書は関数型プログラミングの最初の一冊としては好適ですが，プログラミング全般の最初の一冊としては不適切です．
 
 <!-- Mathematicians who are using Lean as a proof assistant will likely need to write custom proof automation tools at some point.
 This book is also for them.
@@ -53,7 +53,7 @@ Lean でプログラムを書いて実行する前に, 自分のコンピュー
  * `lake` は, `cargo` や `make`, Gradle と同様に, Lean パッケージとその依存関係をビルドします．
  <!-- * `lean` type checks and compiles individual Lean files as well as providing information to programmer tools about files that are currently being written.
    Normally, `lean` is invoked by other tools rather than directly by users. -->
- * `Lean` は、個々の Lean ファイルを型チェックし, コンパイルするだけでなく, プログラマ・ツールに現在書かれているファイルに関する情報を提供します. 通常, Lean はユーザが直接呼び出すのではなく, 他のツールによって呼び出されます.
+ * `Lean` は, 個々の Lean ファイルを型チェックし, コンパイルするだけでなく, プログラマ・ツールに現在書かれているファイルに関する情報を提供します. 通常, Lean はユーザが直接呼び出すのではなく, 他のツールによって呼び出されます.
  <!-- * Plugins for editors, such as Visual Studio Code or Emacs, that communicate with `lean` and present its information conveniently. -->
  * Visual Studio Code や Emacs などのエディタ用のプラグインで，`lean` と通信し, lean の情報を便利に表示することができます.
 
@@ -113,4 +113,4 @@ For example, to enter `α`, type `\alpha`.
 To find out how to type a character in Visual Studio Code, point the mouse at it and look at the tooltip.
 In Emacs, use `C-c C-k` with point on the character in question. -->
 
-デフォルトの Lean の設定では，Visual Studio Code も Emacs も，バックスラッシュ(`\`)の後に名前を続けることでこれらの文字を入力することができます. たとえば `α` と入力するには `\alpha` とタイプします．Visual Studio Code で文字の入力方法を調べるには，マウスをその文字に向けてツールチップを見ればよいです．Emacs の場合、`C-c C-k` を問題の文字にポイントして使います．
+デフォルトの Lean の設定では，Visual Studio Code も Emacs も，バックスラッシュ(`\`)の後に名前を続けることでこれらの文字を入力することができます. たとえば `α` と入力するには `\alpha` とタイプします．Visual Studio Code で文字の入力方法を調べるには，マウスをその文字に向けてツールチップを見ればよいです．Emacs の場合, `C-c C-k` を問題の文字にポイントして使います．