[isabelle-dev] Fwd: A possible bug with Isabelle 2013
nipkow at in.tum.de
Tue Feb 26 18:00:03 CET 2013
Am 26/02/2013 17:37, schrieb Lawrence Paulson:
> That mysterious type always throws me.
> I guess you are saying that this dangling type dependence introduces a function type in the first line. Unfortunately, this is a difficult matter to explain to a student.
I agree. I have yet to see a situation where this implicit introduction of 'a
itself is helpful, let alone intended. Whereas we keep seeing situations where
it first causes confusion and is then eliminated.
> I'll just have to tell him to constrain the types of his bound variables. I believe that the type of X may also be to blame.
Yes, your lambda y is actually a distraction.
> On 26 Feb 2013, at 16:27, Tobias Nipkow <nipkow at in.tum.de> wrote:
>> The two y's are given separate types. In fact, Isabelle introduces ??'a itself
>> in the process.
More information about the isabelle-dev