Spaß for Visual Studio Code：提升第一阶定理证明器的代码体验

Spaß for Visual Studio Code是一款专为第一阶定理证明器Spaß设计的非官方扩展，旨在提供语法高亮和代码片段功能，提升您的代码编写体验。

快速上手

安装扩展后，您可以通过创建扩展名为.dfg、.sps或.spass的新文件，或手动将语言模式设置为Spass来使用其功能。您可以在此处运行代码，或者如果您已安装本地版Spass，则可以通过导航栏中的运行Spass文件按钮、按Ctrl Alt S或使用命令面板中的等效命令来本地运行代码。您可以在此处下载Spass。

注意：为了在本地运行代码，您必须将Spass根文件夹添加到您的PATH中。

功能特性

• 语法高亮：帮助您更清晰地区分代码结构。
• 代码片段：为最常用的功能提供快捷模板，如：
  • 逻辑连接词：and(,)，implies([],)等。
  • 内置函数：predicates[(,)]，functions[(,)]，formula()等。
• 本地代码编译：您可以使用运行Spass文件按钮在本地编译代码。

您可以使用begin_problem()片段将完整的程序模板添加到您的文件中：模板还包含指向在线编译器的链接。

未来功能

• 代码检查（linting）：计划增加此功能，以帮助您编写更高质量的代码。

发布说明

1.2.0版

• 现在可以通过导航栏中的运行Spass文件按钮或使用命令面板中的等效命令在本地编译代码。

1.1.0版

• 用户定义的函数和谓词现在已高亮显示。对begin_problem()片段进行了小幅修改。

1.0.0版

• Spaß扩展的初始发布。