Re: [isabelle] Adding and subtracting functions



There was a discussion of this on the list less than two weeks ago:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-March/msg00016.html
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-March/msg00018.html

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.

- Brian

On Thu, Mar 17, 2011 at 12:44 PM, John Munroe <munddr at gmail.com> wrote:
> 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.