Re: [isabelle] Schematic type variable

On Wed, 19 Oct 2011, Steve Wong wrote:

I'm experimenting with matching a pattern containing schematic type
variables and it'd be great if someone could clarify the following:

ML {*
val trm = @{term "(p::(nat\<Rightarrow>nat) \<Rightarrow> nat) q "};
val pat = @{cpat "?x (?y::?'a)"} |> term_of;
val mtchs = Unify.matchers @{theory} [(pat,trm)] |> Seq.list_of;

May this old thread on isabelle-dev helps: at


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.