lean-ja / lean-by-example

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

`guard_target` を紹介する #410

Open Seasawher opened 3 days ago

Seasawher commented 3 days ago

いままでゴールの状態をチェックするのに show を使っていたが, show は定義上等しい変形を許してしまい,正確なゴール変形を示すことはできない.たとえば dsimp によるゴール状態の変化はチェックできない.

guard_target は構文的に等しいかどうかをチェックできるので,より精密なゴール状態のアサートができる.既存の show によるコードを置き換えることも検討すべき

Seasawher commented 3 days ago

そういう意味では,紛らわしいので show は使わず,change にすべきかもしれない.