Email Gateway (Aug 22 2022 at 11:54): Email Gateway (Aug 22 2022 at 11:54):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I noticed that the private qualifier does not prevent find_theorems from listing the lemma
when the block has ended. I find this irritating, because there is no way to actually use
the lemma. Indeed, if I try to access it, I get an error "Inaccessible fact".
Why should find_theorems list inaccessible facts at all?
My normal use case is to search for theorems that I want to use right now. Private lemmas
are not usable and merely pollute the search results. What other use cases motivate the
current behaviour?
Here is a minimal example:
definition "test = True"
context begin private lemma test: "test" by(simp add: test_def) end
find_theorems test
(* found 2 theorem(s):
Scratch.test: test
Scratch.test_def: test ⟷ True *)
thm Scratch.test (* error "Inaccessible fact" *)
Best,
Andreas
Last updated: Apr 25 2024 at 08:20 UTC