Re: [isabelle] Comparing polymorphic functions

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?

Cheers Christian

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