examples/bts/138.mlw

   1 module Test
   2
   3   use int.Int
   4
   5   type a = < range 22 46 >
   6
   7   let f (b : a) =
   8     requires {a'int b = 42}
   9     ensures {a'int result = a'int b}
  10     (42:a)
  11
  12 end
  13
  14 module Test1
  15   clone Test as T (* Replace with Test does not work *)
  16
  17 end