Zulip Chat Archive

Stream: lean4

Topic: getLCtx and have


Moritz Doll (Nov 30 2022 at 13:15):

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 (Nov 30 2022 at 13:16):

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

Moritz Doll (Nov 30 2022 at 13:20):

that seems indeed to be the issue. Thanks


Last updated: Dec 20 2023 at 11:08 UTC