vscode-lean icon indicating copy to clipboard operation
vscode-lean copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

Add table-of-content and auto-folding for `/-! ## heading`

Open gebner opened this issue 5 years ago • 0 comments

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VSCode.20toc/near/200764479

gebner avatar Jun 13 '20 13:06 gebner