equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 Prolog = FOL + |
11 Prolog = FOL + |
12 types 'a list |
12 types 'a list |
13 arities list :: (term)term |
13 arities list :: (term)term |
14 consts Nil :: "'a list" |
14 consts Nil :: 'a list |
15 ":" :: "['a, 'a list]=> 'a list" (infixr 60) |
15 ":" :: ['a, 'a list]=> 'a list (infixr 60) |
16 app :: "['a list, 'a list, 'a list] => o" |
16 app :: ['a list, 'a list, 'a list] => o |
17 rev :: "['a list, 'a list] => o" |
17 rev :: ['a list, 'a list] => o |
18 rules appNil "app(Nil,ys,ys)" |
18 rules appNil "app(Nil,ys,ys)" |
19 appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" |
19 appCons "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" |
20 revNil "rev(Nil,Nil)" |
20 revNil "rev(Nil,Nil)" |
21 revCons "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" |
21 revCons "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" |
22 end |
22 end |