This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

VScode wishlist

Jump to bottom

Sean Leather edited this page Aug 30, 2018 · 2 revisions

Turn current goal into lemma
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