equal
deleted
inserted
replaced
89 drop_Nil "drop n [] = []" |
89 drop_Nil "drop n [] = []" |
90 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
90 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
91 primrec take list |
91 primrec take list |
92 take_Nil "take n [] = []" |
92 take_Nil "take n [] = []" |
93 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
93 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
94 defs |
94 primrec nth nat |
95 nth_def "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n" |
95 "nth 0 xs = hd xs" |
|
96 "nth (Suc n) xs = nth n (tl xs)" |
96 primrec takeWhile list |
97 primrec takeWhile list |
97 "takeWhile P [] = []" |
98 "takeWhile P [] = []" |
98 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" |
99 "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])" |
99 primrec dropWhile list |
100 primrec dropWhile list |
100 "dropWhile P [] = []" |
101 "dropWhile P [] = []" |