[isabelle] Polymorphic minus



Hi all,

If my understanding is correct, the minus operator has a polymorphic type:
'a => 'a => bool. However, if I have something like:

typedecl T

axiomatization
a :: T
where "a - a = a"

I get an error saying "No type arity T :: minus". So is the minus
polymorphic? The = operator is fine though.

Thanks in advance.

John




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.