Re: [isabelle] Polymorphic minus
> 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