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. Tobias > Larry > > On 26 Feb 2013, at 16:27, Tobias Nipkow <nip...@in.tum.de> wrote: > >> The two y's are given separate types. In fact, Isabelle introduces ??'a >> itself >> in the process. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
