Re: [isabelle] Isabelle2016--1-RC2: Additional name-space pollution via Complex_Main



Hi Johannes,

you are right, having ii as imaginary number is not that strange in
Complex_Main. However, what puzzled me is how it creeped into the
Collections framework, making it omnipresent in many developments
depending on Collections framework directly or indirectly (actually,
many AFP entries). The short answer is:
HOL/Word/Bool_List_Representation now imports Complex_Main: I would
argue that one cannot expect having ii and pi and ... in the namespace
after importing HOL/Word, which is about machine word representation!

So what is the policy to avoid such namespace pollutions? A quick fix
would be adding some hide_const to Bool_List_Representation, but that
would not be very robust ...

--
 Peter




On Fr, 2016-11-18 at 08:13 +0100, Johannes HÃlzl wrote:
> Am Donnerstag, den 17.11.2016, 18:17 +0100 schrieb Peter Lammich:
> > 
> > Hi all,
> > 
> > I realized that by importing Complex_Main, some very short-named
> > constants like "ii" pop up in the global namespace, and thus are
> > not
> > available for variable names any more without explicit fixing. This
> > is
> > very inconvenient. Can't these constants be hidden by default, and
> > only
> > made visible on demand, eg, as we do for Lattice_Syntax?
> > 
> > --
> > Â Peter
> > 
> Hm, "ii" (and \<i>) represent the imaginary number, something one can
> expect from a theory called Complex_Main.
> 
> But as \<i> is also available I think it is okay to hide "ii".
> 
> But is this a problem occurring the first time with Isabelle2016-1-
> RC2?Â
> It should be already available in Isabelle2016 (and before).
> 
> Â- JohannesÂ




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.