Additions to Lean.Meta.Basic

Likely these already exist somewhere. Pointers welcome.

def Lean.Meta.preservingMCtx {α : Type} (x : Lean.MetaM α) : Lean.MetaM α

Restore the metavariable context after execution.

Equations

• Lean.Meta.preservingMCtx x = do let mctx ← Lean.getMCtx tryFinally x (Lean.setMCtx mctx)