Re: [isabelle] Type unification failed



Because 'a is not equal to nat and in the first case you are asking for them
to be the same.

In the second case, f is first specified to be polymorphic then the use, in
"f a", is instantiated appropriately by type inference, that is, you really
have "(f::nat => nat) a", which is allowed because "nat => nat" refines "'a
=> nat".

On Aug 29, 2011 7:42 AM, "John Munroe" <munddr at gmail.com> wrote:
>
> Hi,
>
> Does anyone know why there's a type error in
>
> ML {*
> val trm = @{term "(f::'a=>nat) (a::nat)"};
> *}
>
> but not in
>
> consts
> f:: "'a => nat"
> a :: nat
>
> ML {* @{term "f a" *}
>
> Why are the two cases treated differently?
>
> Thanks
>
> John




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