lean-by-example

LeanByExample ディレクトリ配下の .lean ファイルを編集・追加するときに使う。

.lean ファイルを編集・追加するときにコードの書き方をチェックするために使う。

Lean やそのライブラリの機能、構文、タクティク、コード例、仕様、背景理論を調査するときに使用する。

このリポジトリの実装のために環境構築を新規に行うときに使う。