Julian / Julian/lean.nvim

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

Open
#369 2 comments 0 reactions 0 assignees View on GitHub
enhancement
Dominant language
Lua
Stars
581
Forks
60
Avg merge
4d 12h
Merged PRs (30d)
2

Description

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.

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.