anchor.diff:      in
       aux l1 l2
   
  +(*
  + *  Given `val t : Type` in an interface
  + *  and   `let t = e`    in the corresponding implementation
  + *  The val declaration should contains the `must_erase_for_extraction` attribute
  + *  if and only if `e` is a type that's non-informative (e..g., unit, t -> unit, etc.)
  + *)
  +let check_must_erase_attribute env se =
  +    match se.sigel with
  +    | Sig_let(lbs, l) ->
  +        if not (Options.ide())
  +        then
  +        begin
  +          match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with
  +          | None ->
  +            ()
  +
  +          | Some iface_decls ->
  +            snd lbs |> List.iter (fun lb ->
  +                let lbname = BU.right lb.lbname in
  +                let has_iface_val =
  +                    iface_decls |> BU.for_some (FStar.Parser.AST.decl_is_val lbname.fv_name.v.ident)
  +                in
  +                if has_iface_val
  +                then
  +                    let must_erase =
  +                      TcUtil.must_erase_for_extraction env lb.lbdef in
  +                    let has_attr =
  +                      Env.fv_has_attr env
  +                                      lbname
  +                                      FStar.Parser.Const.must_erase_for_extraction_attr in
  +                    if must_erase && not has_attr
  +                    then
  +                        FStar.Errors.log_issue
  +                            (range_of_fv lbname)
  +                            (FStar.Errors.Error_MustEraseMissing,
  +                                BU.format2
  +                                    "Values of type `%s` will be erased during extraction, \
  +                                    but its interface hides this fact. Add the `must_erase_for_extraction` \
  +                                    attribute to the `val %s` declaration for this symbol in the interface"
  +                                    (Print.fv_to_string lbname)
  +                                    (Print.fv_to_string lbname)
  +                                    )
  +                    else if has_attr && not must_erase
  +                    then FStar.Errors.log_issue
  +                        (range_of_fv lbname)
  +                        (FStar.Errors.Error_MustEraseMissing,
  +                            BU.format1
  +                                "Values of type `%s` cannot be erased during extraction, \
  +                                but the `must_erase_for_extraction` attribute claims that it can. \
  +                                Please remove the attribute."
  +                                (Print.fv_to_string lbname)
  +                                ))
  +    end
  +
  +    | _ -> ()
  +
   let tc_decl' env0 se: list<sigelt> * list<sigelt> * Env.env =
     let env = env0 in
     TcUtil.check_sigelt_quals env se;
  
positive.code:     List.iter (fun se -> env.solver.encode_sig env se) ses';
  
      let exports, hidden =
        check_must_erase_attribute env se;
        if Options.use_extracted_interfaces () then List.rev_append ses' exports, []
        else
          let accum_exports_hidden (exports, hidden) se =
  
negative.code:           then BU.format2 "let %s : %s" (Print.lbname_to_string lb.lbname) (Print.term_to_string (*env*) lb.lbtyp)
            else "") |> String.concat "\n");
  
      check_must_erase_attribute env0 se;
  
      [se], [], env0
  
  (* [tc_decl env se] typechecks [se] in environment [env] and returns *)
  