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?
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.
>> typedecl T
>> a :: T
>> where "a - a = a"
>> I get an error saying "No type arity T :: 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