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.