simp to keep showing the goal state as you type theorems

Stream: lean4 dev

[Joachim Breitner]

This will make a few people happy, I assume :-) (lean4#4177)

Peek-2024-05-15-18-38.mp4

[Floris van Doorn]

This is great!
I think this could be extended further to show a more robust tactic state while typing in other situations. Let me open up a RFC...

[Floris van Doorn]

lean4#4181