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

Commit 0c8d124

Browse files
authored
2.4 Concatenating Streams まで
1 parent 831f79f commit 0c8d124

File tree

1 file changed

+12
-5
lines changed
  • functional-programming-lean/src/hello-world

1 file changed

+12
-5
lines changed

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

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -54,16 +54,23 @@ Once this has been done, `lakefile.lean` should contain: -->
5454

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

57-
## Concatenating Streams
57+
<!-- ## Concatenating Streams -->
5858

59-
Now that the basic skeleton of the program has been built, it's time to actually enter the code.
59+
## ストリームの連結
60+
61+
<!-- Now that the basic skeleton of the program has been built, it's time to actually enter the code.
6062
A proper implementation of `cat` can be used with infinite IO streams, such as `/dev/random`, which means that it can't read its input into memory before outputting it.
6163
Furthermore, it should not work one character at a time, as this leads to frustratingly slow performance.
62-
Instead, it's better to read contiguous blocks of data all at once, directing the data to the standard output one block at a time.
64+
Instead, it's better to read contiguous blocks of data all at once, directing the data to the standard output one block at a time. -->
65+
66+
プログラムの基本的な骨組みができたので,実際にコードを入力するときがきました.`cat` の適切な実装は `/dev/random` のような無限の IO ストリームに使うことができます。これは出力する前に入力をメモリに読み込むことができないことを意味します.さらに,`cat` は一度に1文字ずつ処理すべきではありません.これは非常に遅いパフォーマンスにつながるためです.代わりに,一度に連続したデータブロックを読み取り,そのデータを標準出力に1ブロックずつ送るのがよいでしょう.
6367

64-
The first step is to decide how big of a block to read.
68+
<!-- The first step is to decide how big of a block to read.
6569
For the sake of simplicity, this implementation uses a conservative 20 kilobyte block.
66-
`USize` is analogous to `size_t` in C—it's an unsigned integer type that is big enough to represent all valid array sizes.
70+
`USize` is analogous to `size_t` in C—it's an unsigned integer type that is big enough to represent all valid array sizes. -->
71+
72+
最初のステップはどのくらいの大きさのブロックを読み取るかを決めることです.簡単にするため,この実装では控えめに20キロバイトのブロックを使用します.`USize` は C 言語の `size_t` に類似しており,すべての有効な配列サイズを表すのに十分な大きさの符号なし整数型です.
73+
6774
```lean
6875
{{#include ../../../examples/feline/2/Main.lean:bufsize}}
6976
```

0 commit comments

Comments
 (0)