bench/check-ce/multifile1.mlw

   1
   2 module M
   3   use int.Int
   4
   5   let decr (x: int)
   6     ensures { result < x }
   7   = x - 1
   8
   9   let incr (x: int)
  10     ensures { result > x }
  11   = decr x + 2
  12
  13   val incr_val (x: int) : int
  14     ensures { result > x }
  15
  16 end