Zulip Chat Archive
Stream: lean4 dev
Topic: vscode
Vipin Nair (Sep 20 2023 at 20:23):
I was trying out lean4 with vscode and I noticed the documentation view had some missing documentation. I have a PR that updates the documentation in vscode-lean4 extension - https://github.com/leanprover/vscode-lean4/pull/327
Last updated: May 02 2025 at 03:31 UTC