Skip to content
This repository was archived by the owner on Jan 5, 2025. It is now read-only.

Commit 831f79f

Browse files
authored
2.4 Getting started まで
1 parent 858802c commit 831f79f

File tree

1 file changed

+32
-13
lines changed
  • functional-programming-lean/src/hello-world

1 file changed

+32
-13
lines changed

functional-programming-lean/src/hello-world/cat.md

Lines changed: 32 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1,39 +1,58 @@
1-
# Worked Example: `cat`
1+
<!-- # Worked Example: `cat` -->
22

3-
The standard Unix utility `cat` takes a number of command-line options, followed by zero or more input files.
3+
# 実例:`cat`
4+
5+
<!-- The standard Unix utility `cat` takes a number of command-line options, followed by zero or more input files.
46
If no files are provided, or if one of them is a dash (`-`), then it takes the standard input as the corresponding input instead of reading a file.
57
The contents of the inputs are written, one after the other, to the standard output.
68
If a specified input file does not exist, this is noted on standard error, but `cat` continues concatenating the remaining inputs.
7-
A non-zero exit code is returned if any of the input files do not exist.
9+
A non-zero exit code is returned if any of the input files do not exist. -->
10+
11+
Unix の標準ユーティリティである `cat` はいくつかのコマンドラインオプションと,それに続く0個以上の入力ファイルを受け付けます.ファイルが指定されないか,指定したファイルのうち1つがダッシュ(`-`)の場合,ファイルを読む代わりに標準入力を対応する入力として受け付けます.入力の内容は次々に標準出力に書き出されます.指定した入力ファイルが存在しない場合,そのことが標準エラー出力に表示されますが,`cat` は入力を連結し続けます.存在しない入力ファイルがあったとき,0以外の終了コードが返されます.
812

9-
This section describes a simplified version of `cat`, called `feline`.
13+
<!-- This section describes a simplified version of `cat`, called `feline`.
1014
Unlike commonly-used versions of `cat`, `feline` has no command-line options for features such as numbering lines, indicating non-printing characters, or displaying help text.
11-
Furthermore, it cannot read more than once from a standard input that's associated with a terminal device.
15+
Furthermore, it cannot read more than once from a standard input that's associated with a terminal device. -->
16+
17+
この節では,`feline` と呼ばれる `cat` の簡易版について説明します.一般的なバージョンの `cat` と異なり,`feline` は行番号表示や非印字文字の表示,ヘルプテキストの表示といった機能のコマンドラインオプションはありません.さらに,端末デバイスに関連付けられた標準入力から複数回読み込むこともできません.
1218

13-
To get the most benefit from this section, follow along yourself.
19+
<!-- To get the most benefit from this section, follow along yourself.
1420
It's OK to copy-paste the code examples, but it's even better to type them in by hand.
15-
This makes it easier to learn the mechanical process of typing in code, recovering from mistakes, and interpreting feedback from the compiler.
21+
This makes it easier to learn the mechanical process of typing in code, recovering from mistakes, and interpreting feedback from the compiler. -->
22+
23+
この節で最大限の効果を得るには,自分自身でコードを書いてください.コード例をコピーペーストしてもかまいませんが,手書きで入力することを推奨します.そうすることで,コードを入力し,ミスから回復し,コンパイラからのフィードバックを解釈するという機械的なプロセスを学びやすくなります.
24+
25+
<!-- ## Getting started -->
1626

17-
## Getting started
27+
## はじめる
1828

19-
The first step in implementing `feline` is to create a package and decide how to organize the code.
29+
<!-- The first step in implementing `feline` is to create a package and decide how to organize the code.
2030
In this case, because the program is so simple, all the code will be placed in `Main.lean`.
2131
The first step is to run `lake new feline`.
2232
Edit the Lakefile to remove the library, and delete the generated library code and the reference to it from `Main.lean`.
23-
Once this has been done, `lakefile.lean` should contain:
33+
Once this has been done, `lakefile.lean` should contain: -->
34+
35+
`feline` 実装の最初のステップは,パッケージを作成し,コードをどのように整理するかを決めることです.今回の場合,プログラムは非常に簡単なので,すべてのコードは `Main.lean` に書きます.最初のステップは `lake new feline` を実行することです.Lakefile を編集してライブラリを削除し,生成されたライブラリコードとその参照を `Main.lean` も削除します.
36+
これが完了すると,`lakefile.lean` は次のようになります:
2437

2538
```lean
2639
{{#include ../../../examples/feline/1/lakefile.lean}}
2740
```
2841

29-
and `Main.lean` should contain something like:
42+
<!-- and `Main.lean` should contain something like: -->
43+
44+
そして `Main.lean` も次のようになります:
45+
3046
```lean
3147
{{#include ../../../examples/feline/1/Main.lean}}
3248
```
33-
Alternatively, running `lake new feline exe` instructs `lake` to use a template that does not include a library section, making it unnecessary to edit the file.
49+
<!-- Alternatively, running `lake new feline exe` instructs `lake` to use a template that does not include a library section, making it unnecessary to edit the file. -->
50+
51+
あるいは,`lake new feline exe` を実行すると `lake` にライブラリセクションを含まないテンプレートを使用するように指示されるため,ファイルを編集する必要がなくなります.
3452

35-
Ensure that the code can be built by running `{{#command {feline/1} {feline/1} {lake build} }}`.
53+
<!-- Ensure that the code can be built by running `{{#command {feline/1} {feline/1} {lake build} }}`. -->
3654

55+
`{{#command {feline/1} {feline/1} {lake build} }}` を実行してコードがビルドできることを確認してください.
3756

3857
## Concatenating Streams
3958

0 commit comments

Comments
 (0)