getLCtx and have

Stream: lean4

[Moritz Doll]

If I add something to the context using have : h' : α := sorry, then the output of getLCtx is unchanged (I can provide an #mwe, but it is really ugly, because I didn't bother to get it to pretty print, I only count hypotheses). I would expect to see a LocalDecl added, but why is this not happening.
Context: SolveByElim/applyAssumption don't find assumptions that have been recently added using have

[Jannis Limperg]

Maybe you forgot to use mvarId.withContext or withMainContext after the have?

[Moritz Doll]

that seems indeed to be the issue. Thanks