equal
deleted
inserted
replaced
78 length_Nil "length([]) = 0" |
78 length_Nil "length([]) = 0" |
79 length_Cons "length(x#xs) = Suc(length(xs))" |
79 length_Cons "length(x#xs) = Suc(length(xs))" |
80 primrec flat list |
80 primrec flat list |
81 flat_Nil "flat([]) = []" |
81 flat_Nil "flat([]) = []" |
82 flat_Cons "flat(x#xs) = x @ flat(xs)" |
82 flat_Cons "flat(x#xs) = x @ flat(xs)" |
|
83 primrec drop list |
|
84 drop_Nil "drop n [] = []" |
|
85 drop_Cons "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)" |
|
86 primrec take list |
|
87 take_Nil "take n [] = []" |
|
88 take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)" |
83 defs |
89 defs |
84 drop_def "drop n == nat_rec n (%xs.xs) \ |
|
85 \ (%m r xs. case xs of [] => [] | y#ys => r ys)" |
|
86 take_def "take n == nat_rec n (%xs.[]) \ |
|
87 \ (%m r xs. case xs of [] => [] | y#ys => y # r ys)" |
|
88 nth_def "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))" |
90 nth_def "nth(n) == nat_rec n hd (%m r xs. r(tl(xs)))" |
89 end |
91 end |