--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Fri Oct 19 07:48:25 2007 +0200
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex Fri Oct 19 09:59:46 2007 +0200
@@ -36,8 +36,11 @@
{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
The syntax is rather self-explanatory: We introduce a function by
- giving its name, its type and a set of defining recursive
- equations.%
+ giving its name, its type,
+ and a set of defining recursive equations.
+ If we leave out the type, the most general type will be
+ inferred, which can sometimes lead to surprises: Since both \isa{{\isadigit{1}}} and \isa{plus} are overloaded, we would end up
+ with \isa{fib\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ {\isacharprime}a{\isacharcolon}{\isacharcolon}{\isacharbraceleft}one{\isacharcomma}plus{\isacharbraceright}}.%
\end{isamarkuptext}%
\isamarkuptrue%
%