[isabelle-dev] Binding with implicit rename
florian.haftmann at informatik.tu-muenchen.de
Tue Oct 26 11:24:15 CEST 2010
> However in packages often also bindings are created automatically.
> Currently I am working on some fragements of a mechanism which analyzes
> parts of a theory (most prominently constants and theorems) and
> generated new constants and theorems from them. The result, in
> particular the new constants, are highly unpredictable, and the user is
> not really interested in the number or names of the new constants. The
> situation is somehow similar to the predicate compiler, but even less
> tamed. To ensure that the new constants do not clash with existing
> ones, the bindings for them have to be distilled carefully and a rather
> unsatisfactory way. I am asking myself whether this could be
> dramatically simplified by giving bindings a »liberal« flag: this could
> be set e.g. using a function Binding.liberal :: binding -> binding; on
> declaration in a namespace, the basename of a liberal binding would be
> modified if it would clash with an existing declaration. User-space
> binding would stay non-liberal an issue an error on clashing.
After some internal discussion I have come to the conclusion that this
is actually a bad idea since then a theory would contain things which
are supposed to be used in user space but not referenced by explicit
text. I think now the best solution is to have optional explicit names
given by the user.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev