anchor.diff:      None (Range.union_ranges wp_t.pos wp_e.pos) in
     mk_comp ed u_a a wp [], Env.trivial_guard
   
  +(*
  + * PURE<u> t (fun _ -> False)
  + *
  + * This is the comp type for a match with no cases (used in bind_cases)
  + *)
  +let comp_pure_wp_false env (u:universe) (t:typ) =
  +  let post_k = U.arrow [null_binder t] (S.mk_Total U.ktype0) in
  +  let kwp    = U.arrow [null_binder post_k] (S.mk_Total U.ktype0) in
  +  let post   = S.new_bv None post_k in
  +  let wp     = U.abs [S.mk_binder post]
  +               (fvar_const env C.false_lid)
  +               (Some (U.mk_residual_comp C.effect_Tot_lid None [TOTAL])) in
  +  let md     = Env.get_effect_decl env C.effect_PURE_lid in
  +  mk_comp md u t wp []
  +
   let bind_cases env0 (res_t:typ)
     (lcases:list<(formula * lident * list<cflag> * (bool -> lcomp))>)
     (scrutinee:bv) : lcomp =
  
positive.code:             (*
               * The formula in each of the branches of lcases is the branch condition of *just* that branch,
               *   e.g. match e with | C -> ... | D -> ...
               *     the formula in the two branches is is_C e and is_D e
               *
               * branch_conditions below builds a list where the formulas are composite
               *   and include the negation of previous branches, e.g.
               *   is_C e and (not (is_C e) /\ is_D e)
               *
               * these will be used to weaken the lift guards when combining the branches
               *
               *   (we need it because the braches are combined using fold_right)
               *
               * note that we don't need to build these just to combine cases because the shape of if_then_else
               *   (p ==> ...) /\ (not p ==> ...) takes care of it
               *)
              let branch_conditions =
                lcases
                |> List.map (fun (g, _, _, _) -> g)
                |> List.fold_left (fun (conds, acc) g ->
                    let cond = U.mk_conj acc (U.mk_neg g) in
                    (conds@[cond]), cond) ([U.t_true], U.t_true)
                |> fst
                |> List.splitAt (List.length lcases)
                |> fst in
  
              //let default_case, g_comp = weaken_comp env default_case default_branch_condition in
  
              let md, comp, g_comp = List.fold_right2 (fun (g, eff_label, _, cthen) bcond (_, celse, g_comp) ->
                  let cthen, gthen = TcComm.lcomp_comp (maybe_return eff_label cthen) in
                  let gthen = TcComm.weaken_guard_formula gthen (U.mk_conj bcond g) in
                  let md, ct_then, ct_else, g_lift_then, g_lift_else =
                    let m, cthen, celse, g_lift_then, g_lift_else =
                      lift_comps_sep_guards env cthen celse None false in
                    let md = Env.get_effect_decl env m in
                    md, cthen |> U.comp_to_comp_typ, celse |> U.comp_to_comp_typ, g_lift_then, g_lift_else in
                  let fn =
                    if md |> U.is_layered then mk_layered_conjunction
                    else mk_non_layered_conjunction in
  
                  //weaken the lift guards
                  let g_lift_then = TcComm.weaken_guard_formula g_lift_then (U.mk_conj bcond g) in
                  let g_lift_else = TcComm.weaken_guard_formula g_lift_else (U.mk_conj bcond (U.mk_neg g)) in                
                  let g_lift = Env.conj_guard g_lift_then g_lift_else in
  
                  let c, g_conjunction = fn env md u_res_t res_t g ct_then ct_else (Env.get_range env) in
                  Some md,
                  c,
                  Env.conj_guards [g_comp; gthen; g_lift; g_conjunction]
              ) lcases branch_conditions (None, default_case, Env.trivial_guard) in
  
              //close g_comp with the scrutinee bv
              let g_comp = Env.close_guard env0 [scrutinee |> S.mk_binder] g_comp in
  
negative.code:         then
               lax_mk_tot_or_comp_l eff u_res_t res_t [], Env.trivial_guard
          else begin
              let maybe_return eff_label_then cthen =
                 if should_not_inline_whole_match
                 || not (is_pure_or_ghost_effect env eff)
  