Email Gateway (Aug 22 2022 at 18:02): Email Gateway (Aug 22 2022 at 18:02):From: Peter Zeller <p_zeller@cs.uni-kl.de>
Hello *,
I wanted to report a small usability problem I face from time to time.
Here is a short example:
lemma
shows "P ⟶ R"
proof
have a: "P ⟶ R"
sorry ― ‹Assume there is some complex proof here.›
assume a: P
show R
find_theorems R ― ‹Finds nothing.›
sledgehammer ― ‹Does not find proof.›
using a and P ⟶ R by simp
qed
The problem is that I accidentally gave the same name to 2 local facts
and find_theorems and sledgehammer can no longer find the first fact,
although it is still referable with quotes.
I think it would be good for usability if those facts still appeared in
search and were found by sledgehammer. Alternatively it would also be
helpful to get a warning when shadowing other local facts.
When shadowing local variables there can also be problems, so a warning
would also be nice in that case.
Regards,
Peter
Last updated: Apr 23 2024 at 16:19 UTC