equal
deleted
inserted
replaced
1 (* basic examples *) |
1 (* basic examples *) |
2 |
2 |
3 Test = HOHH + |
3 Test = HOHH + |
4 |
4 |
5 types nat |
5 types nat |
6 arities nat :: term |
6 arities nat :: type |
7 |
7 |
8 types 'a list |
8 types 'a list |
9 arities list :: (term) term |
9 arities list :: (type) type |
10 |
10 |
11 consts Nil :: 'a list ("[]") |
11 consts Nil :: 'a list ("[]") |
12 Cons :: 'a => 'a list => 'a list (infixr "#" 65) |
12 Cons :: 'a => 'a list => 'a list (infixr "#" 65) |
13 |
13 |
14 syntax |
14 syntax |
18 translations |
18 translations |
19 "[x, xs]" == "x#[xs]" |
19 "[x, xs]" == "x#[xs]" |
20 "[x]" == "x#[]" |
20 "[x]" == "x#[]" |
21 |
21 |
22 types person |
22 types person |
23 arities person :: term |
23 arities person :: type |
24 |
24 |
25 consts |
25 consts |
26 append :: ['a list, 'a list, 'a list] => bool |
26 append :: ['a list, 'a list, 'a list] => bool |
27 reverse :: ['a list, 'a list] => bool |
27 reverse :: ['a list, 'a list] => bool |
28 |
28 |