Leanのドキュメント
Leanのドキュメント
どれから読めばいいのか分からなくてムカつくmiyamonz.icon
Core Documentation
モナドの話とかいるのか？
next stepに他のドキュメントへのリンクが有る
数学の形式化
TPILより先にこっちを読むべき。先に説明書を全部読むタイプならTPIL読んでもいいよって書いてある
これはある程度動かしたあとに読むと良さそうだ
Lean は対話型定理証明システムであり、依存型理論を基盤としています。最先端の数学研究からソフトウェア検証まで、幅広い用途を想定して設計されています。
言語のリファレンスなんで、細かい概念の説明や挙動を知りたいときに読むべきか
TPILなどから個別の型の解説として飛べる
Further reading
...
Interactive Games and Tutorials
Resources
ドキュメントや教材など
これ、公式からリンクが辿れないが、どこから？
これ古いドキュメントなのか?
This PR removes the old documentation overview site, as its content has moved to the main Lean website infrastructure.
main infraってどこ？
これ、外部へリンクしてるだけか
これいいなmiyamonz.icon
文法を学ぶのにはいい
少し前より整えられた気がするmiyamonz.icon
Leanを学ぶためには
言語自体の入門部分
Haskellっぽい部分
依存型理論
さらに、その型システムが数学の命題や証明と結びつけられること
実際に証明をどういう流れで記述するか
という要素があって、頭から書くのが難しいのだろう
簡単な証明をいくつか実際に書くのが良いのだが
そう感じるのは、miyamonz.iconがすでにHaskellの文法の雰囲気を知っているからかもしれない