[isabelle-dev] Bad binding warnings
makarius at sketis.net
Thu Jul 14 21:20:34 CEST 2011
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.
More information about the isabelle-dev