-
Notifications
You must be signed in to change notification settings - Fork 298
VScode wishlist
Johan Commelin edited this page Nov 13, 2019
·
2 revisions
-
Turn current goal intoDone bylemma
extract_goal
. - Help with naming conventions
- Help with formatting
- Translate between tactic and term-mode proofs
- After typing identifier, insert the correct number of _s based on the number of explicit arguments to the function
- Hotkey switches to @-identifier and inserts _s in the correct places
- Editor tells you if you have written a rfl lemma and it inserts the proof for you