「定理証明支援系Lean」の版間の差分
Notion-MW |
Notion-MW |
||
| 180行目: | 180行目: | ||
=== パッケージ(lake) === | === パッケージ(lake) === | ||
<code>lake new | <code>lake new パッケージ名（パッケージ名と同じ名前のフォルダが作成され、その中にパッケージができる）</code>、または<code>lake init パッケージ名（パッケージはカレントディレクトリに作成される）</code>を実行。詳しいやり方は[https://github.com/leanprover-community/mathlib4 https://github.com/leanprover-community/mathlib4] とか。 | ||
lakeのドキュメントはここ [https://github.com/leanprover/lean4/tree/master/src/lake https://github.com/leanprover/lean4/tree/master/src/lake] | lakeのドキュメントはここ [https://github.com/leanprover/lean4/tree/master/src/lake https://github.com/leanprover/lean4/tree/master/src/lake] | ||