
effect Exc : (unit -> unit)
effect Other : (unit -> unit)

let f () 
(*@  requires (true, emp, ())   @*)
@   ensures   ( true , ( Exc!).(Other!).Other?().Exc ? ( ) , ( ) ) @
= 
  let x = perform Exc in 
  let y = perform Other in 
  y ();
  x ()

let handler 
(*@  requires (true, emp, ())   @*)
@   ensures   ( true , (  ) , ( ) ) @
= 
  match f () with 
  | x -> x
  | effect Exc k -> () 


   ( Exc!).(Other!).Other?().Exc ? ( ) 
    his          current ev         continuation ( k )            bindings 
 1   emp           (  ! )           ( Other!).Other?().Exc ? ( )    
 2   Exc          
 ---------------------------------- 
  

  (Exc!).(Other!).Other?().Exc?()
   his         current ev        continuation (k)           bindings 
1  emp          (Exc!)          (Other!).Other?().Exc?()    
2  Exc          
----------------------------------
Exc
*)
@  requires (true, emp, ())   @
@  requires (true, emp, ())   @

effect Exc : (unit -> unit)
effect Other : (unit -> unit)

let f () 
@   ensures   ( true , ( Exc!).(Other!).Other?().Exc ? ( ) , ( ) ) @
= 
  let x = perform Exc in 
  let y = perform Other in 
  y ();
  x ()

let handler 
@   ensures   ( true , (  ) , ( ) ) @
= 
  match f () with 
  | x -> x
  | effect Exc k -> () 


   ( Exc!).(Other!).Other?().Exc ? ( ) 
    his          current ev         continuation ( k )            bindings 
 1   emp           (  ! )           ( Other!).Other?().Exc ? ( )    
 2   Exc          
 ---------------------------------- 
  

  (Exc!).(Other!).Other?().Exc?()
   his         current ev        continuation (k)           bindings 
1  emp          (Exc!)          (Other!).Other?().Exc?()    
2  Exc          
----------------------------------
Exc
*)