Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] private still pollutes theory namespace

Email Gateway (Aug 22 2022 at 10:35):

From: Peter Lammich <lammich@in.tum.de>
Hi,

when I use private, e.g. in
theory T imports Main begin
context begin
private lemma foo: "..."
end

after the context,
the lemma foo is still visible to find_theorems (as T.foo).
Moreover, I cannot name any other lemma in theory T foo, even not a
second private one:
lemma foo: "..." *** Duplicate fact declaration

context begin
private lemma foo: "..." *** Duplicate fact declaration

Is this the desired behaviour of "private", or just an imperfect
implementation due to other/technical constraints?

Email Gateway (Aug 22 2022 at 10:35):

From: Lars Hupel <hupel@in.tum.de>
Dear Peter,

Is this the desired behaviour of "private", or just an imperfect
implementation due to other/technical constraints?

I haven't yet looked too closely how "private" works, but the behaviour
appears to be consistent with "hide_fact":

lemma foo: "True" ..
hide_fact foo

thm foo (* error *)
find_theorems True name: foo (* lists Scratch.foo *)

lemma foo: "True" .. (* error: duplicate *)

The only difference I found is in the error message produced by "thm foo".

Cheers
Lars

Last updated: Apr 23 2024 at 08:19 UTC