anchor.diff:       delta_level=d;
        primitive_steps=built_in_primitive_steps;
        strong=false;
  -     memoize_lazy=true}
  +     memoize_lazy=true;
  +     normalize_pure_lets=
  +       (Options.normalize_pure_terms_for_extraction()
  +        || not (s |> List.contains PureSubtermsWithinComputations))}
   
   let normalize_with_primitive_steps ps s e t =
       let c = config s e in
  
positive.code:           | Tm_let((false, [lb]), body) ->
              let n = TypeChecker.Env.norm_eff_name cfg.tcenv lb.lbeff in
              if not (cfg.steps |> List.contains NoDeltaSteps)
              && ((U.is_pure_effect n
                   && (not (cfg.steps |> List.contains PureSubtermsWithinComputations)
                       || Options.normalize_pure_terms_for_extraction()))
                  || (U.is_ghost_effect n
                      && not (cfg.steps |> List.contains PureSubtermsWithinComputations)))
              then let binder = S.mk_binder (BU.left lb.lbname) in
  
negative.code:     delta_level: list<Env.delta_level>;  // Controls how much unfolding of definitions should be performed
      primitive_steps:list<primitive_step>;
      strong : bool;                       // under a binder
      memoize_lazy : bool;
      normalize_pure_lets: bool;
  }
  
  type branches = list<(pat * option<term> * term)>
  