equal
deleted
inserted
replaced
14 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
14 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
15 filter :: ['a => bool, 'a list] => 'a list |
15 filter :: ['a => bool, 'a list] => 'a list |
16 concat :: 'a list list => 'a list |
16 concat :: 'a list list => 'a list |
17 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b |
17 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b |
18 hd :: 'a list => 'a |
18 hd :: 'a list => 'a |
19 length :: 'a list => nat |
|
20 set_of_list :: 'a list => 'a set |
19 set_of_list :: 'a list => 'a set |
21 list_all :: ('a => bool) => ('a list => bool) |
20 list_all :: ('a => bool) => ('a list => bool) |
22 map :: ('a=>'b) => ('a list => 'b list) |
21 map :: ('a=>'b) => ('a list => 'b list) |
23 mem :: ['a, 'a list] => bool (infixl 55) |
22 mem :: ['a, 'a list] => bool (infixl 55) |
24 nth :: [nat, 'a list] => 'a |
23 nth :: [nat, 'a list] => 'a |
51 intrs |
50 intrs |
52 Nil "[]: lists A" |
51 Nil "[]: lists A" |
53 Cons "[| a: A; l: lists A |] ==> a#l : lists A" |
52 Cons "[| a: A; l: lists A |] ==> a#l : lists A" |
54 |
53 |
55 |
54 |
|
55 (*Function "size" is overloaded for all datatypes. Users may refer to the |
|
56 list version as "length".*) |
|
57 syntax length :: 'a list => nat |
|
58 translations "length" => "size" |
|
59 |
56 primrec hd list |
60 primrec hd list |
57 "hd([]) = arbitrary" |
61 "hd([]) = arbitrary" |
58 "hd(x#xs) = x" |
62 "hd(x#xs) = x" |
59 primrec tl list |
63 primrec tl list |
60 "tl([]) = arbitrary" |
64 "tl([]) = arbitrary" |
85 "filter P [] = []" |
89 "filter P [] = []" |
86 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" |
90 "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)" |
87 primrec foldl list |
91 primrec foldl list |
88 "foldl f a [] = a" |
92 "foldl f a [] = a" |
89 "foldl f a (x#xs) = foldl f (f a x) xs" |
93 "foldl f a (x#xs) = foldl f (f a x) xs" |
90 primrec length list |
|
91 "length([]) = 0" |
|
92 "length(x#xs) = Suc(length(xs))" |
|
93 primrec concat list |
94 primrec concat list |
94 "concat([]) = []" |
95 "concat([]) = []" |
95 "concat(x#xs) = x @ concat(xs)" |
96 "concat(x#xs) = x @ concat(xs)" |
96 primrec drop list |
97 primrec drop list |
97 drop_Nil "drop n [] = []" |
98 drop_Nil "drop n [] = []" |