tactic mode holes

Stream: general

[Reid Barton]

Do holes and hole commands not work inside a tactic block, or is it just an emacs thing?

[Reid Barton]

If I have exact _ inside a tactic and try to use a hole command, I get an error indicating the Lean server didn't think there was a hole there, I believe.
If I use exact {! _ !} instead then the hole seems to be treated as sorry (?)

[Bryan Gin-ge Chen]

Yeah, they don't work, unfortunately.

[Reid Barton]

ok, not just me, then