Re: [isabelle] Comparing polymorphic functions

Thanks for the reply.

Could someone please add to why schematic type variables can't be specialised? Why don't they behave like type variables?



On Jan 27, 2011 12:19pm, Eg Gloor <egglue at> wrote:
On Thu, Jan 27, 2011 at 12:14 PM, Christian Maeder Christian.Maeder at> wrote:

Am 27.01.2011 12:58, schrieb Eg Gloor:

> type variables? If I do something similar with schematic types:


> schematic_lemma test: "(x::?'a=>?'b=>?'c) = (y::?'d=>?'e)"


> I get a type unification error there. It seems ?'e can't be specialised

> to "?'b => ?'c" in this case.

I'm no Isabelle expert, but I suspect that the types are already

specialized differently. Does "(x::?'a) = (y::?'d)" work?

No, neither does "(x::?'a) = (y::real)". I suspect there's no polymorphism with schematic types...


Cheers Christian

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