`proof_wanted`の利用法の詳細を書く

lean-ja / lean-by-example

コード例で学ぶ Lean 言語

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

MIT License

39 stars 7 forks source link

Open SnO2WMaN opened 3 months ago

SnO2WMaN commented 3 months ago

現状，「proof_wantedで作られた定理を実際問題どうやって使うか」に関する記載が無い．

記憶では，simp属性などを付けて明示的には参照せずに使うといったのが大抵の使い方だった覚えがある．

Seasawher commented 3 months ago

提案ありがとうございます．具体的なコード例を提供していただけますか？

SnO2WMaN commented 3 months ago

simp属性などを付けて試してみたが上手く具体例を提示できなかった．もしかしたら自分の記憶と用例が変わっているかもしれない．（自分も他のリポジトリ（思い出せない）で使っているのを見たことがあるだけなので）