lean.nvim icon indicating copy to clipboard operation
lean.nvim copied to clipboard

Still show last compiled goal-state while `Processing file...`

Open valeratrades opened this issue 1 year ago • 2 comments

When I'm writing a proof, I would love to be able to have a consistent point of reference of existing hypothesis in the scope. Currently on every justification step I have to stop, wait for the file to process, and then in 90% of cases look for a hypothesis that was already available to find its name and exact statement.

It would be so much faster to have an option (or have it be default) of seeing the previously compiled state with a small indicator of Processing file... at the bottom or to the side, which would allow to write proofs without needless interrupts.

valeratrades avatar Dec 15 '24 11:12 valeratrades