anchor.diff:    | Some x -> f x
     | None -> d
   
  -(* We memoize the normal form of variables in the environment, in
  - * order to implement call-by-need and avoid an exponential explosion,
  - * but we take care to only reuse memoized values when the cfg has not
  - * changed. The main reason is normalization requests, which can "grow"
  - * the set of allowed computations steps, and hence we may memoize
  - * something during the request that is used outside of it. This will
  - * essentially make it invalid. See issue #2155 in Github.
  - *
  - * We compare the cfg with physical equality, so it has to be the
  - * exact same object in memory. See read_memo and set_memo below. *)
  -type cfg_memo<'a> = memo<(Cfg.cfg * 'a)>
  -
   type closure =
  -  | Clos of env * term * cfg_memo<(env * term)> * bool //memo for lazy evaluation; bool marks whether or not this is a fixpoint
  +  | Clos of env * term * memo<(env * term)> * bool //memo for lazy evaluation; bool marks whether or not this is a fixpoint
     | Univ of universe                               //universe terms do not have free variables
     | Dummy                                          //Dummy is a placeholder for a binder when doing strong reduction
   and env = list<(option<binder>*closure)>
  
positive.code:                    let stack =
                       stack |>
                       List.fold_right (fun (a, aq) stack ->
                         Arg (Clos(env, a, BU.mk_ref (Some (cfg, ([], a))), false),aq,t.pos)::stack)
                       norm_args
                     in
                     log cfg  (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args));
  
negative.code: type stack_elt =
   | Arg      of closure * aqual * Range.range
   | UnivArgs of list<universe> * Range.range
   | MemoLazy of memo<(env * term)>
   | Match    of env * branches * cfg * Range.range
   | Abs      of env * binders * env * option<residual_comp> * Range.range //the second env is the first one extended with the binders, for reducing the option<lcomp>
   | App      of env * term * aqual * Range.range
  