feat: make sure `clear_value` preserves local context order (#8792) This PR makes the `clear_value` tactic preserve the order of variables in the local context. This is done by adding `Lean.MVarId.withRevertedFrom`, which reverts all local variables starting from a given variable, rather than only the ones that depend on it. Note: an alternative implementation might convert the ldecl to a cdecl and then reset the meta cache. This assumes that there are no other caches that might still remember the value of the ldecl.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean.