unit print_list (l: <int> 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: <int[0,5]> 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 ();
}