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
> 
> axiomatization
> 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"
begin

...

end

Cheers,
René
-- 
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.