use int.Int type list 'a = Nil | Cons 'a (list 'a) function append (l1:list 'a) (l2:list 'a) : list 'a = match l1 with | Nil -> l2 | Cons x l -> Cons x (append l l2) end (* lemma append_nil: forall l:list 'a. append l Nil = l lemma append_assoc: forall l1 l2 l3:list 'a. append (append l1 l2) l3 = append l1 (append l2 l3) *) function length (l:list 'a) : int = match l with | Nil -> 0 | Cons _ r -> 1 + length r end (* lemma length_nonneg: forall l:list 'a. length l >= 0 *) function rev (l:list 'a) : list 'a = match l with | Nil -> Nil | Cons x r -> append (rev r) (Cons x Nil) end val ref l : list int let rec rev_append (r:list int) : unit variant { 0 } writes { } ensures { true } = match r with | Nil -> () | Cons x r -> l <- Cons x l; rev_append r end let reverse (r:list int) : unit writes { l } ensures { l = rev r } = l <- Nil; () (* to be completed *)