equal
deleted
inserted
replaced
9 List = Divides + |
9 List = Divides + |
10 |
10 |
11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
12 |
12 |
13 consts |
13 consts |
14 pred_list :: "('a list * 'a list) set" |
|
15 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
14 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
16 filter :: ['a => bool, 'a list] => 'a list |
15 filter :: ['a => bool, 'a list] => 'a list |
17 concat :: 'a list list => 'a list |
16 concat :: 'a list list => 'a list |
18 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b |
17 foldl :: [['b,'a] => 'b, 'b, 'a list] => 'b |
19 hd :: 'a list => 'a |
18 hd :: 'a list => 'a |
51 inductive "lists A" |
50 inductive "lists A" |
52 intrs |
51 intrs |
53 Nil "[]: lists A" |
52 Nil "[]: lists A" |
54 Cons "[| a: A; l: lists A |] ==> a#l : lists A" |
53 Cons "[| a: A; l: lists A |] ==> a#l : lists A" |
55 |
54 |
56 |
|
57 rules |
|
58 pred_list_def "pred_list == {(x,y). ? h. y = h#x}" |
|
59 |
55 |
60 primrec hd list |
56 primrec hd list |
61 "hd([]) = arbitrary" |
57 "hd([]) = arbitrary" |
62 "hd(x#xs) = x" |
58 "hd(x#xs) = x" |
63 primrec tl list |
59 primrec tl list |