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?

Thanks

Eg

On Jan 27, 2011 12:19pm, Eg Gloor <egglue at gmail.com> wrote:
On Thu, Jan 27, 2011 at 12:14 PM, Christian Maeder Christian.Maeder at dfki.de> 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...


Thanks
Eg



Cheers Christian









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