Lean 構文早見表

Lean 構文早見表(Lean by Example) は,Lean の基本的な構文や機能を紹介するためのサンプルコード集です.Lean の数多くの機能の全体を概観できる資料となることを目指しています.

本書は逆引きタクティクリストの姉妹編です.mathlibにあるタクティクや,# 付きの対話的コマンドについてはあちらを参照してください.