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 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...
This archive was generated by a fusion of
Pipermail (Mailman edition) and