examples/bts/13853b.mlw

   1
   2 (*
   3
   4 BTS 13853 (follow-up)
   5
   6 https://gforge.inria.fr/tracker/?func=detail&atid=10293&aid=13853&group_id=2990
   7
   8 *)
   9
  10
  11 module T
  12
  13   type t
  14
  15   exception MyExc
  16
  17   let rec f (_x:t) : t raises { MyExc } = raise MyExc
  18   with g  (x:t) : (_r: t) raises { MyExc } ensures { true } = f x
  19 end
  20