Leanのベストプラクティス - Githubissues

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

https://lean-ja.github.io/lean-by-example/

MIT License

39 stars 7 forks source link

Leanのベストプラクティス #190

Open Seasawher opened 4 months ago

Seasawher commented 4 months ago

関数ではなくて定理に制約をつける
忘却継承 forgetful inheritance
構造体ではなく型クラスで代数構造を定義する

Seasawher commented 3 months ago

表記法を定義するとき、まずは型クラスを定義する

Seasawher commented 3 months ago

証明の最後以外ではsimpを避けて simp only にする（これはlinterが存在する）