Names

The STELF naming convention changes in a number of ways from the original Twelf conventions (note that text in italics is not yet finished)

Module Syntax

The syntax for module types remains the same, with all caps SIGN. A difference is that, however, while in SML these can be written in sig files, in OCaml, these are written in SIGN.ml files, which correspond Sign.ml which implements it. Module Syntax likewise stays the same. The largest difference (and a large one) is that functors should start with the work Make_ followed by an underscore, ie, Make_AST. Note that the rest of the name should still be UpperCamelCase

Module Renamings

A number of modules now have different names, or are split apart. The largest change is that of lambda and frontend, each of which bears completely different names in the new source. lambda is split into two libraries, one still called lambda, which defines functions like whnf, and also Syntax, which defines STELF's abstract syntax (what was IntSyn). In accordance with this, while the alias IntSyn is provided, Ast and AST are prefered

The external syntax got an even bigger change. Firstly, the reconstruction phase and parsing phase and the external syntax have their own library (actually, for parsing libraries) apiece. Reconstruction gets moved into the library Recon, the various external syntaxes (with heavy changes, see ???) are now CST, and the parsing phase is (primarly) in Modern. In addition, the toplevel has been moved to PAL (Pi forAll Lambda, the constructs of LP) and is now a full REPL

Term Syntax

Terms should be in lower_snake_case, as should types. If a term has _ at the end, it probably is a leftover