Email Gateway (Aug 18 2022 at 17:24): Email Gateway (Aug 18 2022 at 17:24):From: John Munroe <munddr@gmail.com>
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
Email Gateway (Aug 18 2022 at 17:24):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Last updated: Apr 20 2024 at 12:26 UTC