term-mode assumption fails on no goals

Stream: lean4

[Aaron Liu]

Is this intended?
● Separation.lean - mathlib4 - Visual Studio Code 11_1_2025 18_22_45.png
I suspect it will be a while before I can get a #mwe out of this.

[Robin Arnez]

I guess it tells you to replace it with an _?