[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 17:11:57 CEST 2013
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
?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
More information about the isabelle-dev