anchor.diff:        let (t, ae, s) = infer_exp env e (Some et) in
         let ae = AEOp (Uop UOld, [ae], tv, et) in
         (tv, ae, s@[(t, tv)])
  +    | EOp (Uop (UIs x), [e]) ->
  +      let x = Id ("uu___is_"+ (string_of_id x)) in
  +      let e = EApply (x, [e]) in
  +      let (t, ae, s) = infer_exp env e expected_typ in
  +      let ae = 
  +        match ae with 
  +        | AEApply (x, es, [t], [et]) -> AEOp (Uop (UIs x), es, t, et)
  +        | _ -> err ("expect apply expression") in
  +      (t, ae, s)
  +    | EOp (Uop op, _) ->
  +      err ("unsupported Uop")
       | EOp (Bop op, [e1; e2]) when isArithmeticOp op ->
         // op in {+, -, *, /, %} 
         let tv = next_type_var() in
  
positive.code:   | (TApp (x, ys), TApp (u, vs)) -> 
      let tc = List.fold2 (fun (l:typ_constraints) t1 t2 -> l@[(t1, t2)]) [] ys vs in
      unify env m ([(x, u)]@tc)
    | (TName (Id x), TName (Id y)) -> 
      if x = y then m else err ("type mismatch ")
    | _ -> err ("type mismatch ")
  
negative.code:   push_scope_mod env (Const (id, t))
     
  let push_rets (env:env) (rets:pformal list):env =
    {env with scope_mods = List.fold (fun s (x, t, g, io, a) -> Variable (x, (base_typ t)):: s) env.scope_mods rets}
  
  let push_params_without_rets (env:env) (args:pformal list) (rets:pformal list):env =
    let arg_in_rets arg l = List.exists (fun elem -> elem = arg) l in
  