search

lean-ja / lean-by-example

コード例で学ぶ Lean 言語
https://lean-ja.github.io/lean-by-example/
MIT License
15 stars 5 forks source link

属性はいつ削除できるのか #384

Open Seasawher opened 6 days ago

Seasawher commented 6 days ago

simp 属性は削除できるが，他の属性は削除できないこともある．いつ削除できるのか？どうやって判定するのか？

Seasawher commented 4 days ago

コマンド attribute [-instance] を使えば、現在のセクションや名前空間が閉じられるまで、あるいは現在のファイルの終わりまで、指定したインスタンスを一時的に無効化することもできる。

see TPiL: https://aconite-ac.github.io/theorem_proving_in_lean4_ja/type_classes.html?highlight=irreducible#local-instances-%E3%83%AD%E3%83%BC%E3%82%AB%E3%83%AB%E3%82%A4%E3%83%B3%E3%82%B9%E3%82%BF%E3%83%B3%E3%82%B9

属性を永続的に削除することはできなくて，一時的にデバッグ用に削除できるだけ