VSCode到达 这是证明助手的非官方VSCode扩展,由。 由于唯一的官方编辑器是IntelliJ IDEA,所以当我们想享受VSCode如此出色的启动速度时,这很难。 所以,我做这个很有趣。 语法突出显示文件来自 ,此插件中捆绑的Arend编译器使用Arend的最新开发版本。 如果您想要稳定的版本,则可以构建它,并为自己的jar指定VSCode设置arend.languageServer.path 。 设置 您需要安装Java(版本> = 11),插件将尝试按(按顺序)在其中找到: VSCode配置java.home 环境变量JAVA_HOME 环境变量PATH 如果某些方法不