examples/sorted_list.mlw

   1 (* Find a value in a sorted list of integers *)
   2
   3 module FindInSortedList
   4
   5   use int.Int
   6   use list.List
   7   use list.Mem
   8   use list.SortedInt
   9
  10   lemma Sorted_not_mem:
  11     forall x y : int, l : list int.
  12     x < y -> sorted (Cons y l) -> not mem x (Cons y l)
  13
  14   let rec find x l
  15     requires { sorted l }
  16     variant { l }
  17     ensures { result=True <-> mem x l }
  18   = match l with
  19     | Nil -> False
  20     | Cons y r -> x = y || x > y && find x r
  21     end
  22
  23 end