add [@@no_inline_let] annotation for local lets

src/parser/FStar.Parser.Const.fst

@@ -346,6 +346,7 @@ let steps_unmeta        = psconst "unmeta"
 let deprecated_attr = pconst "deprecated"
 let warn_on_use_attr = pconst "warn_on_use"
 let inline_let_attr = p2l ["FStar"; "Pervasives"; "inline_let"]
+let no_inline_let_attr = p2l ["FStar"; "Pervasives"; "no_inline_let"]
 let rename_let_attr = p2l ["FStar"; "Pervasives"; "rename_let"]
 let plugin_attr     = p2l ["FStar"; "Pervasives"; "plugin"]
 let tcnorm_attr    =  p2l ["FStar"; "Pervasives"; "tcnorm"]

src/syntax/FStar.Syntax.Util.fst

@@ -1298,6 +1298,7 @@ let tac_opaque_attr = exp_string "tac_opaque"
 let dm4f_bind_range_attr = fvar_const PC.dm4f_bind_range_attr
 let tcdecltime_attr = fvar_const PC.tcdecltime_attr
 let inline_let_attr = fvar_const PC.inline_let_attr
+let no_inline_let_attr = fvar_const PC.no_inline_let_attr
 let rename_let_attr = fvar_const PC.rename_let_attr
 
 let t_ctx_uvar_and_sust = fvar_const PC.ctx_uvar_and_subst_lid

src/typechecker/FStar.TypeChecker.Cfg.fst

@@ -374,13 +374,15 @@ let should_reduce_local_let cfg lb =
   else if cfg.steps.pure_subterms_within_computations &&
           U.has_attribute lb.lbattrs PC.inline_let_attr
   then true //1. we're extracting, and it's marked @inline_let
+  else if U.has_attribute lb.lbattrs PC.no_inline_let_attr
+  then false //Or, 2. do not unfold as it's explicitly marked as @no_inline_let
   else
     let n = Env.norm_eff_name cfg.tcenv lb.lbeff in
     if U.is_pure_effect n &&
        (cfg.normalize_pure_lets
         || U.has_attribute lb.lbattrs PC.inline_let_attr)
-    then true //Or, 2. it's pure and we either not extracting, or it's marked @inline_let
-    else U.is_ghost_effect n && //Or, 3. it's ghost and we're not extracting
+    then true //Or, 3. it's pure and we are either not extracting, or it's marked @inline_let
+    else U.is_ghost_effect n && //Or, 4. it's ghost and we're not extracting
          not (cfg.steps.pure_subterms_within_computations)
 
 let translate_norm_step = function

ulib/FStar.Pervasives.fst

@@ -141,6 +141,8 @@ let rec false_elim #_ _ = false_elim ()
 
 let inline_let = ()
 
+let no_inline_let = ()
+
 let rename_let _ = ()
 
 let plugin _ = ()

ulib/FStar.Pervasives.fsti

@@ -846,6 +846,12 @@ type __internal_ocaml_attributes =
     size. *)
 val inline_let : unit
 
+(** The [no_inline_let] attribute on a local let-binding prevents the
+    normalizer from unfolding the definition of a local let-binding. This
+    attribute can be useful when processing definitions with tactics, as
+    otherwise the normalizer will eagerly unfold all pure definitions. *)
+val no_inline_let : unit
+
 (** The [rename_let] attribute support a form of metaprogramming for
     the names of let-bound variables used in extracted code.