Mercurial > urweb

comparison tests/termination.ur @ 313:e0ed0d4dabc9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Termination checking
author Adam Chlipala <adamc@hcoop.net>
date Tue, 09 Sep 2008 11:46:33 -0400
parents
children
comparison
equal deleted inserted replaced
312:f387d12193ba 313:e0ed0d4dabc9
1 datatype list a = Nil | Cons of a * list a
2
3 fun isNil (t ::: Type) (ls : list t) : bool =
4 case ls of
5 Nil => True
6 | Cons _ => False
7
8 fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
9 case ls1 of
10 Nil => ls2
11 | Cons (x, ls1') => Cons (x, append ls1' ls2)
12
13 fun appendR (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
14 case ls1 of
15 Nil => ls2
16 | Cons (x, ls1') => Cons (x, appendR ls2 ls1')
17
18 (*fun naughty (t ::: Type) (ls : list t) : list t = naughty ls*)
19
20 fun append1 (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
21 case ls1 of
22 Nil => ls2
23 | Cons (x, ls1') => Cons (x, append2 ls2 ls1')
24
25 and append2 (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
26 case ls1 of
27 Nil => ls2
28 | Cons (x, ls1') => Cons (x, append1 ls1' ls2)