[isabelle-dev] Bad binding warnings
makarius at sketis.net
Fri Jul 15 00:56:36 CEST 2011
On Thu, 14 Jul 2011, Lars Noschinski wrote:
> On 14.07.2011 21:20, Makarius wrote:
>> 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.
> Is it to be expected, that this warning now occurs quite often in a lemma
> statement, even if Auto Quickcheck and Solve are disabled?
It is expected in the sense that the "more thorough" check of 9bd8d4addd6e
should help to isolate boundary cases and sort them out. See now
1183951365de and 1c18d52204be. More fine points are to be expected.
BTW, one of the oddities of the too liberal old scheme is the confusion
caused by things like datatype foo = "nat * bool". It was also possible
to define constructors called "" or " " or " " etc.
More information about the isabelle-dev