Is the following behavior of Kananaskis-5 correct?
-
HOL-4 [Kananaskis 5 (built Fri Nov 28 13:45:15 2008)]
For introductory HOL help, type: help "hol";
-
[
Hi Peter,
Your example is actually a first order matching problem and
the first order matcher fails:
> match_term ``\x:'a. y:'b`` ``\x:num. x + x`` handle e => Raise e;
>
> Exception raised at Term.raw_match_term error:
> variable bound by scope
The higher order matcher should fail but returns
Hi Peter,
| It seems unreasonable that these two terms should match, since then the
| instantiation of the pattern term (as shown above using the results of the
| higher order match) does not in fact produce the target term.
In HOL Light, at least, this is a known "feature", and I guess HOL4 has
