Feature request: controlling `[@inline_let]` via normalization flags

With @Kachoc we are working on a Noise protocol compiler embedded within the F\* normalizer (details in a forthcoming submission!). One of the key ideas is that many core actions of the protocol are written as functions of the form:

```
let process_message (pat: Noise.pattern): process_message_t pat =
...
```

and are expected to be partially evaluated after being applied to their first argument. This is an embedded compiler, in the sense that the whole term "compiles" (partially reduces) on F\*'s normalizer in order to yield a specialized `process_message` for a specific noise pattern.

This relies on the fanciest possible combinations of attributes, namely `[@inline_let]`s, `norm`, `zeta_full` and many other recent technological advancements.

One thing that came up is that it's generally easier to debug partial evaluation via a post-processing tactic rather than relying on `inline_for_extraction` everywhere. The former allows "seeing" the term, potentially tweaking the flags "live", rather than relying on the whole extraction pipeline, which can have a very, very long debug-extract-edit cycle.

One key discrepancy, however, is that post-processing tactics don't *exactly* allow replicating what would otherwise happen at extraction-time. This is because `inline_for_extraction` and `[@inline_let]` don't generally get triggered via post-processing tactics, but happen at a later phase -- to the best of my knowledge, the user doesn't have a way to replicate that. The internal flag is not exposed to the user, and the internal flag is only used directly from the F\*'s extraction modules. The same goes for `[@inline_let]`.

What would be greatly helpful for us is if we could trigger those reduction steps from a post-processing tactic; that way, we could debug partial evaluation completely within the interactive mode, and have a much more efficient way to go about these things than generating a .checked file, extracting a whole file, looking at the OCaml code, and trying to figure out whether the reduction step we wanted to see happened.

Hope this makes sense! Thanks,

Jonathan

Start by reading the F* normalizer and extraction modules, especially how post-processing tactics handle normalization flags and how inline_for_extraction and inline_let are applied. Define the user-facing mechanism for triggering these reductions interactively, then verify that post-processing can reproduce the relevant extraction-time behavior without requiring a full extraction cycle.

Written by the indexing model from the issue text.