Style Guide
The style for STELF code varies a fair bit from the original Twelf style.
The %scope command took a lot of time to perfect.
Please use it, no more add-nat-zero, use scopes, it’ll look cleaner as %(zero nat add).
In addition, avoid the charecter _ in names, altough it is fine. Use - instead, as it is more readable and lines up with the conventions of Twelf among other languages 1.
Unlike in Twelf, the following practices regarding name encodings should be followed:
- Write descriptive names, abbreviations are fine, but must be understandable. Again, if you find yourself feeling the need to write a name that is too long, the answer is probably scopes.
- While you may use
/and-in names, consider if you really should be. The common uses of/and-were both for creating names that would be ambiguous in short form. - The full UTF8 charecter set is at your disposal2, so use it! Rather than
to, consider any of the following alternatives->(no longer reserved)→(unicode looks nice)
Outer Mode
Section titled “Outer Mode”The outer mode syntax is minimal for a reason.
Unlike the inner syntax, here there are only two reserved classes, % and whitespace.
This means there’s no need to comment out your code!
Indeed, the Neovim plugin for STELF automatically highlights the outer mode syntax as Markdown.
Of course, you can use any typesetting system that doesn’t use the charecter %
A couple notes about the outer mode syntax:
- While not strictly neccassary in every case, it is recommended to preceed outer mode by the stop command and a newline
%. - Comments should be avoided, and instead outer mode should be used to explain the code.