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