> 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.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
