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: http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg01173.html


	Makarius





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