自動的にめいっぱい generalize する induction タクティクはないのか？

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

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

MIT License

51 stars 7 forks source link

Open Seasawher opened 3 weeks ago

Seasawher commented 3 weeks ago

理論上は作れるはず

Seasawher commented 3 weeks ago

generalizing * という構文でめいっぱい generalize する機能がほしい

Seasawher commented 3 weeks ago