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 { ? } writes { l } ensures { ? } = 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; ? (* Local Variables: compile-command: "why3 ide rev.mlw" End: *)