Skip to content

Commit

Permalink
README 更新
Browse files Browse the repository at this point in the history
  • Loading branch information
Seasawher committed Sep 23, 2024
1 parent 6171191 commit 2811e68
Showing 1 changed file with 6 additions and 2 deletions.
8 changes: 6 additions & 2 deletions src/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,17 @@ lean-ja の Discord サーバが[こちら](https://discord.gg/p32ZfnVawh)にあ
## 本書の特色 😎

### 1. 内容が正確
本書のすべての Lean コードブロックはバージョン `{{#include ../lean-toolchain}}` で実際にエラーなく動くことを CI で確認しています。動かないコード例を見つけられた際はお手数ですが issue でご報告をお願いします。
Lean は開発が活発に続いているソフトウェアであり、毎月のように新しいリリースが行われています。その際破壊的な変更が行われることは少なくありません。

しかし、本書のほぼすべての Lean コードブロックはバージョン `{{#include ../lean-toolchain}}` で実際にエラーなく動くことを確認済みです。動かないコード例を見つけられた際はお手数ですが issue でご報告をお願いします。

### 2. 情報が新しい
本書には、Lean とそのライブラリのバージョンを自動で更新するワークフローが設定されており、定期的にバージョンを最新のものに更新しています。Lean の最新情報をすべて掲載することはかないませんが、最新の情報を提供できるよう努めています。

### 3. コードをすぐに試せる
本書のすべての Lean コードブロックは、マウスを重ねると Lean Playground へジャンプするボタン <a class="fa fa-external-link"></a> が現れるようになっています。またコードブロックの中には、`import` 文が足りないなどの理由でそのままでは実行できないものがありますが、そうした場合は画面右上の実行ボタン <i class="fa fa-play"></i> をクリックしていただければ、ファイル全体を実行することができます。
本書のすべての Lean コードブロックは、マウスを重ねると Lean Playground へジャンプするボタン <i class="fa fa-external-link"></i> が現れるようになっています。

またコードブロックの中には、`import` 文が足りないなどの理由でそのままでは実行できないものがありますが、そうした場合は画面右上の実行ボタン <i class="fa fa-play"></i> をクリックしていただければ、ファイル全体を実行することができます。

## スポンサー

Expand Down

0 comments on commit 2811e68

Please sign in to comment.