Re: [isabelle] Type unification failed



It should be said that types explicitly provided in type annotations in term
quotations are not unified by the type checker, they are simply left as they
are, whereas implicit types in term quotations are unified.

on 29/8/11 8:07 AM, Ramana Kumar <rk436 at cam.ac.uk> wrote:

> 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.