module ConwaySort

val sorted: list int -> Tot bool
  let rec sorted l = match l with
      | [] -> true
      | [x] -> true
      | x::y::xs -> x <= y && sorted (y::xs)

let input = [6; 8; 3; 9; 5; 4; 1; 7; 0; 2]

val sort: list int -> Tot (m:list int{sorted m})
let sort l = [15; 16; 17; 18; 19; 20]