equal
deleted
inserted
replaced
10 \isa{bool}, the result is a binary tree; if it is instantiated to |
10 \isa{bool}, the result is a binary tree; if it is instantiated to |
11 \isa{nat}, we have an infinitely branching tree because each node |
11 \isa{nat}, we have an infinitely branching tree because each node |
12 has as many subtrees as there are natural numbers. How can we possibly |
12 has as many subtrees as there are natural numbers. How can we possibly |
13 write down such a tree? Using functional notation! For example, the term |
13 write down such a tree? Using functional notation! For example, the term |
14 \begin{isabelle}% |
14 \begin{isabelle}% |
15 \ \ \ \ \ Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}% |
15 \ \ \ \ \ Branch\ {\isadigit{0}}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}% |
16 \end{isabelle} |
16 \end{isabelle} |
17 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose |
17 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose |
18 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and |
18 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and |
19 has merely \isa{Tip}s as further subtrees. |
19 has merely \isa{Tip}s as further subtrees. |
20 |
20 |