I will tackle your questions one at a time.
The difficulty with your original question concerns, what do we mean by
higher-order matching? For Isabelle, these are nothing but unifiers which leave
the object unchanged.
The problem is that you are trying to match ?x ?y against ?f ?stuff and
On 19/11/10 12:28, Lawrence Paulson wrote:
Looking at this again, I'm not certain there is a bug. You are displaying the
variable assignments, but are you first applying the type variable assignments?
Both must be used in order to instantiate the object term.
Please bear with me -- I'm not
On 19/11/10 14:10, Lawrence Paulson wrote:
If you look at the file Pure/envir.ML, you will find the definition of
environments (which has separate components for the two assignments) as well as
primitives that you should use to apply an environment to a term. If you only
look at assignments
Indeed I find the code peculiar, in that it delivers the higher-order matchers
followed by the first-order ones. But these are different things. And I imagine
there is often redundancy.
Larry
On 19 Nov 2010, at 15:50, Michael Chan wrote:
On 19/11/10 14:10, Lawrence Paulson wrote:
If you look
On Fri, 19 Nov 2010, Lawrence Paulson wrote:
Indeed I find the code peculiar, in that it delivers the higher-order
matchers followed by the first-order ones. But these are different
things. And I imagine there is often redundancy.
Unify.matchers started as Isar-specific
