equal
deleted
inserted
replaced
5 In particular, there are @{text"case"}-expressions, for example |
5 In particular, there are @{text"case"}-expressions, for example |
6 @{term[display]"case n of 0 => 0 | Suc m => m"} |
6 @{term[display]"case n of 0 => 0 | Suc m => m"} |
7 primitive recursion, for example |
7 primitive recursion, for example |
8 *} |
8 *} |
9 |
9 |
10 consts sum :: "nat \<Rightarrow> nat" |
10 primrec sum :: "nat \<Rightarrow> nat" where |
11 primrec "sum 0 = 0" |
11 "sum 0 = 0" | |
12 "sum (Suc n) = Suc n + sum n" |
12 "sum (Suc n) = Suc n + sum n" |
13 |
13 |
14 text{*\noindent |
14 text{*\noindent |
15 and induction, for example |
15 and induction, for example |
16 *} |
16 *} |
17 |
17 |