On Thu, 14 Jul 2011, Lukas Bulwahn wrote:
Working with the development version, I have been noticing warnings "...
Bad binding: ...". Is there now a stricter guideline using or creating
bindings that Isabelle's developers should follow?
Not "now", they have been there for several years already. Formal
entities within the term language need to observe proper identifier
syntax. I cannot quote the many problems with totally arbitrary names on
the spot, because it is such a long time ago when this was still done
routinely (like global constants "op +" or "op *").
Recently I've noticed that internal "fixes" where accidentally omitted
from the binding check. There were also some incidents and genuine
programming errors introduced due to the absence of a proper check.
For example, Variable.add_fixes with type variables 'a 'b etc. simply does
not make any sense. Now you get a warning at least. See also the
somewhat compact explanation of type variables vs. term variables in in
the implementation manual section 5.1.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
