Unofficial sintax highlighting and code snippets extension for Spaß first order theorem prover.
Once the extension is installed, you can use its features by creating a new file with the .dfg
, .sps
or .spass
extension or by manually setting the language mode to Spass. You can run your code here or you can run it locally if you have a local installation of Spass by using the Run Spass file button in the navbar, by pressing Ctrl+Alt+S or by using the equivalent command in the command palette. You can download Spass here.
! in order to run your code locally you must add Spass root folder to your PATH
- syntax higlighting
- code snippets for the most used function such as
- Logical connectives
and(,)
,implies([],)
etc. - built-in functions
predicates[(,)].
,functions[(,)].
,formula().
- Logical connectives
- local code compiling
you can use
begin_problem().
snippet to add a full program template to your file: the template also contains a link to the online compiler
- linting
Code can be compiled locally by using the Run Spass file button in the navbar or by using the equivalent command in the command palette
User-defined functions and predicates are now highlited. Minor changes to begin_problem().
snippet
Initial release of Spaß extension