From 5e4e047c33b2aee276ac88cc81c25ca58ac6f2c1 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 21 Oct 2023 20:55:18 +0900 Subject: [PATCH] =?UTF-8?q?=E5=8F=A5=E8=AA=AD=E7=82=B9=E3=81=8C=E7=B5=B1?= =?UTF-8?q?=E4=B8=80=E3=81=95=E3=82=8C=E3=81=A6=E3=81=84=E3=81=AA=E3=81=84?= =?UTF-8?q?=E3=83=9F=E3=82=B9=E3=82=92=E4=BF=AE=E6=AD=A3?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../src/getting-to-know/evaluating.md | 4 ++-- .../src/getting-to-know/functions-and-definitions.md | 4 ++-- functional-programming-lean/src/getting-to-know/types.md | 2 +- functional-programming-lean/src/introduction.md | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/functional-programming-lean/src/getting-to-know/evaluating.md b/functional-programming-lean/src/getting-to-know/evaluating.md index 22fcbdc9..15cde709 100644 --- a/functional-programming-lean/src/getting-to-know/evaluating.md +++ b/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}} diff --git a/functional-programming-lean/src/getting-to-know/functions-and-definitions.md b/functional-programming-lean/src/getting-to-know/functions-and-definitions.md index 8c3da05d..c2b86b9a 100644 --- a/functional-programming-lean/src/getting-to-know/functions-and-definitions.md +++ b/functional-programming-lean/src/getting-to-know/functions-and-definitions.md @@ -3,7 +3,7 @@ -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 で関数を定義するには様々な方法があります．最もシン -関数が各引数の間にスペースを書くことで複数の引数に適用されるように, 複数の引数を受け付ける関数は, 引数の名前と型の間にスペースを入れることで定義されます．関数 `maximum` は，2つの引数の最大値を返すもので，2つの `Nat` 型引数 `n` と `k` を取り、`Nat` を返します． +関数が各引数の間にスペースを書くことで複数の引数に適用されるように, 複数の引数を受け付ける関数は, 引数の名前と型の間にスペースを入れることで定義されます．関数 `maximum` は，2つの引数の最大値を返すもので，2つの `Nat` 型引数 `n` と `k` を取り, `Nat` を返します． ```lean {{#example_decl Examples/Intro.lean maximum}} diff --git a/functional-programming-lean/src/getting-to-know/types.md b/functional-programming-lean/src/getting-to-know/types.md index c636bd24..f4e08a1b 100644 --- a/functional-programming-lean/src/getting-to-know/types.md +++ b/functional-programming-lean/src/getting-to-know/types.md @@ -77,7 +77,7 @@ provide it directly: --> -式を評価せずに型を確かめるには、`#eval` の代わりに `#check` を使います．例えば +式を評価せずに型を確かめるには, `#eval` の代わりに `#check` を使います．例えば ```lean {{#example_in Examples/Intro.lean oneMinusTwoIntType}} diff --git a/functional-programming-lean/src/introduction.md b/functional-programming-lean/src/introduction.md index 0ba99d8b..818fbe95 100644 --- a/functional-programming-lean/src/introduction.md +++ b/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# などの関数型言語に精通していることは必須ではありません．一方，本書はループ・関数・データ構造など，ほとんどのプログラミング言語に共通する概念の知識を前提としています．本書は関数型プログラミングの最初の一冊としては好適ですが，プログラミング全般の最初の一冊としては不適切です． - * `Lean` は、個々の Lean ファイルを型チェックし, コンパイルするだけでなく, プログラマ・ツールに現在書かれているファイルに関する情報を提供します. 通常, Lean はユーザが直接呼び出すのではなく, 他のツールによって呼び出されます. + * `Lean` は, 個々の Lean ファイルを型チェックし, コンパイルするだけでなく, プログラマ・ツールに現在書かれているファイルに関する情報を提供します. 通常, Lean はユーザが直接呼び出すのではなく, 他のツールによって呼び出されます. * 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` を問題の文字にポイントして使います． \ No newline at end of file +デフォルトの Lean の設定では，Visual Studio Code も Emacs も，バックスラッシュ(`\`)の後に名前を続けることでこれらの文字を入力することができます. たとえば `α` と入力するには `\alpha` とタイプします．Visual Studio Code で文字の入力方法を調べるには，マウスをその文字に向けてツールチップを見ればよいです．Emacs の場合, `C-c C-k` を問題の文字にポイントして使います． \ No newline at end of file