the disagreement pairs should be fully eta-expanded by this point, though I haven't looked at the code recently. That would imply that the body_type cannot be a function type.
Larry On 28 May 2013, at 16:11, Makarius <[email protected]> wrote: > On Tue, 28 May 2013, Lawrence Paulson wrote: > >> I don't quite understand your commentary, because the result of body_type >> can never be a function. >> >> In general, polymorphism in higher-order unification never instantiates a >> type variable to a function type, for the reason you seem to hint at: >> because you wouldn't know when to stop. This is a source of incompleteness, >> but it has always been there. > > The function type could have been there already from the start, e.g.: > > ?x i j k :: ?'a => ?'b > > for > > ?x :: U => V => W => ?'a => ?'b > > where i :: U, j :: V, k :: W in the term context. > > In that case, the unrestricted body_type would merely take ?'b into account > of the unification problem, not the remaining ?'a => ?'b. > > > It is just a habit of mine to watch out for such incidents -- we used to have > them in many situations in the past when traversing ==> of the logic. And of > course, such doubts are no disproof of anything, just critical observations. > > > Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
