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
