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?

Thank you
John

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