effect Foo : (unit -> unit)


let f () 
(*@ requires _^* @*)
@ ensures    . Q(Foo ( ) ) @
  = perform Foo ()

let res 
  (*@ requires _^* @*)
@ ensures    @
  =
  match f () with
  | _ -> ()
  | effect Foo k ->  continue k (fun () -> ())

@ requires _^* @
@ requires _^* @
effect Foo : (unit -> unit)


let f () 
@ ensures    . Q(Foo ( ) ) @
  = perform Foo ()

let res 
@ ensures    @
  =
  match f () with
  | _ -> ()
  | effect Foo k ->  continue k (fun () -> ())
