Re: [isabelle] Polymorphic minus



> I see. But
> 
> fixes a :: "'T :: minus"
> 
> means that a is assigned to a type variable 'T rather than a concrete
> type T. What if a is of a concrete type?

Then this type T has to be in the class minus, 
otherwise you cannot write "a - a".

René

> 2011/9/20 René Thiemann <rene.thiemann at uibk.ac.at>:
>>> If my understanding is correct, the minus operator has a polymorphic type:
>>> 'a => 'a => bool. However, if I have something like:
>> 
>> But 'a must have sort minus.
>> 
>> I would start as follows
>> 
>> locale test =
>>  fixes a :: "'T :: minus"
>>  assumes ax1: "a - a = a"
>> begin

-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck






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