summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/TutorialI/fp.tex

changeset 10237 | 875bf54b5d74 |

parent 10181 | c07860c826c5 |

child 10396 | 5ab08609e6c8 |

--- a/doc-src/TutorialI/fp.tex Tue Oct 17 13:28:57 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Tue Oct 17 16:59:02 2000 +0200 @@ -188,11 +188,12 @@ Every datatype $t$ comes equipped with a \isa{size} function from $t$ into the natural numbers (see~\S\ref{sec:nat} below). For lists, \isa{size} is just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs + - 1}. In general, \isa{size} returns \isa{0} for all constructors that do -not have an argument of type $t$, and for all other constructors \isa{1 +} -the sum of the sizes of all arguments of type $t$. Note that because + 1}. In general, \isaindexbold{size} returns \isa{0} for all constructors +that do not have an argument of type $t$, and for all other constructors +\isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because \isa{size} is defined on every datatype, it is overloaded; on lists -\isa{size} is also called \isa{length}, which is not overloaded. +\isa{size} is also called \isaindexbold{length}, which is not overloaded. +Isbelle will always show \isa{size} on lists as \isa{length}. \subsection{Primitive recursion}