tests/test_ghost.mlw

   1
   2
   3 module M
   4
   5   type t = O | S t
   6
   7   let f () =
   8      let ghost g (x:t) : t =
   9         match x with O -> O | S y -> y end
  10 (*
  11      with ghost h (x:t) : t =
  12         match x with O -> O | S y -> y end
  13 *)
  14      in
  15      ()
  16
  17 end