perf: give `currRecDepth` its own `ReaderT` layer in `CoreM` This PR stops the recursion-depth guard from rebuilding `Core.Context` on every recursive step. Roughly 96% of `Core.Context` reconstructions exist only to bump the depth counter, and each one paid a reference count increment per pointer field. `withReader` can never reuse the `Context` record, so keeping `currRecDepth` there made every `withIncRecDepth` rebuild it. As its own reader layer the depth is just an extra argument, so a recursion step neither allocates nor touches a reference count. The layer sits inside the `Context` reader so that a bare `read` still resolves to `Context`, and `CoreM.run` gains an initial-depth parameter so nested command elaboration keeps inheriting its caller's depth. Note this changes `CoreM`'s arity, which is externally observable in LCNF output.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.