[isabelle] Adding and subtracting functions



Hi,

I have a question about the plus and minus operators. It seems that
the minus operator is polymorphic and the following works:

lemma "(f::nat=>nat) = g - h"

whereas,

lemma "(f::nat=>nat) = g + h" gives an error saying

"*** No type arity fun :: plus
*** At command "lemma""

Likewise for times.

Aren't all times, plus and minus polymorphic?

Thanks

John





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