We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
PPContext.runMetaM
1 parent f84b4e3 commit 7bcb6fdCopy full SHA for 7bcb6fd
src/Lean/Meta/Basic.lean
@@ -2703,7 +2703,8 @@ def runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
2703
{ env := ppCtx.env, ngen := { namePrefix := `_pp_uniq } }
2704
2705
def runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
2706
- ppCtx.runCoreM <| x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
+ ppCtx.runCoreM <|
2707
+ (withPopulatingLocalInstances x).run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
2708
2709
end PPContext
2710
0 commit comments