lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
15 stars 5 forks source link

本書の特色を加筆する #306

Closed Seasawher closed 1 week ago

Seasawher commented 2 weeks ago

コントリビュータや読者向けの方針を書いていく

  1. コード例で書かれた内容を検証する

leanのアップデートに追従するにはそうするしかない。逆に言えば、コード例で検証できないことは書かないということになる。

本書が理論的なことに深く立ち入らないのはこのため。 また、コード例ベースにするのには「わかりやすく、実践的な内容になる」という嬉しい効果もある。

  1. 各項目が互いに依存しないようにする

これは長期的に保守、開発を行っていくため。「初めから順に読まないといけない」ようにするなど、各項目に依存関係があると変更すべき箇所が多くなりがちで破綻も起こりやすい。各項目に依存がなければ変更範囲はローカルなのでわかりやすい。

調べたいときに調べたいことだけさっと読めるという副次的なメリットもある。FPiLなどは最初から順に読まなければいけないので、知りたいことがどこに書いてあるかわからなかったり、見つけても前の章を読まないといけなかったりする。

Seasawher commented 2 weeks ago

「はじめに」の本書の特色のところに追記していきたい。

Seasawher commented 1 week ago

情報の探しやすさ

TPiLやメタプロ、fp lean などに分散している情報を1箇所にまとめ、leanの仕様についてのあらゆる疑問について、探しやすいリファレンスになる(のが目標)

Seasawher commented 1 week ago

目標をミニマルにするため,控えめに書くことにする