Since you all were great last time: What are your favorite tools for proof development in an interactive theorem prover? What ideas do you find promising for future tooling?
Conversation
the Lean VSCode IDE and project/package tools for Lean are both a pleasure to use.
Hopefully features like intelligent code completion, jump to/peek definition, and better search tools will find their way to other provers.
1
6
I can second that - super snappy! Just wish it had more Agda-style stuff like nice case splitting.
