summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | krauss |

Fri, 19 Oct 2007 09:59:46 +0200 | |

changeset 25091 | a2ae7f71613d |

parent 25090 | 4a50b958391a |

child 25092 | 1d7616d74095 |

Updated function tutorial: Types can be inferred and need not be given anymore

--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Fri Oct 19 07:48:25 2007 +0200 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Fri Oct 19 09:59:46 2007 +0200 @@ -23,8 +23,12 @@ text {* 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 @{term + "1::nat"} and @{text plus} are overloaded, we would end up + with @{text "fib :: nat \<Rightarrow> 'a::{one,plus}"}. *} text {*

--- 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% %