Re: [isabelle] Adding and subtracting functions
There was a discussion of this on the list less than two weeks ago:
The short answer is that "+" and "*" for functions are defined in
~~/src/HOL/Library/Function_Algebras.thy. This is not a dependency of
Main, so you need to import it explicitly.
On Thu, Mar 17, 2011 at 12:44 PM, John Munroe <munddr at gmail.com> wrote:
> 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"
> 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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and