unit print_list (l: list) { var: int x;; while (true) { switch (l) { case Nil: print_string ("[]"); break; case Cons (x, l): print_int (x); print_string ("::"); } } } ('a){m:nat, n:nat} <'a> list(m+n) rev_append (xs: <'a> list(m), ys: <'a> list(n)) { var: 'a x;; invariant: [m1:nat,n1:nat | m1+n1 = m+n] (xs: <'a> list(m1), ys: <'a> list(n1)) while (true) { switch (xs) { case Nil: return ys; case Cons(x, xs): ys = Cons(x, ys); } } exit; } ('a){m:nat, n:nat} <'a> list(m+n) revApp (xs: <'a> list(m), ys: <'a> list(n)) { var: 'a x;; invariant: [m1:nat,n1:nat | m1+n1=m+n] (xs: <'a> list(m1), ys: <'a> list(n1)) while (true) { switch (xs) { case Nil: break; case Cons(x, xs): ys = Cons(x, ys); } } withinv (ys: <'a> list(m+n)) return ys; } ('a){n:nat} <'a> list(n) reverse (xs: <'a> list(n)) { return revApp(xs, Nil); } unit main () { var: l: list;; l = Cons (3, Cons(5, Cons (2, Nil))); l = Cons (3, Cons(5, Cons (2, l))); print_list (l); print_newline (); l = reverse (l); print_list (l); print_newline (); }