LocalInstances in InfoTree contexts

Stream: lean4

[Eric Wieser]

I'm trying to run some MetaM code from data in an InfoTree, but it seems that docs#Lean.Elab.TermInfo does not hold the LocalInstances that I need to run synthInstance in that MetaM code. I can probably get to where I need to be by using docs#Lean.Meta.withLocalInstances, but it's not obvious to me how to get the required List Lean.LocalDecl from a docs#Lean.LocalContext.

[Eric Wieser]

I guess (withLocalInstances lctx.decls.toList.reduceOption f).run { lctx := lctx } { mctx := info.mctx } is what I want, instead of the incorrect contents of docs#Lean.Elab.ContextInfo.runMetaM ?