Lexical analysis of Twelf has purposely been kept simple, with few reserved characters and identifiers. As a result one may need to use more whitespace to separate identifiers than in other languages. For example, `A->B' or `A+B' are single identifiers, while `A -> B' and `A + B' both consist of 3 identifiers.
During parsing, identifiers are resolved as reserved identifiers, constants, bound variables, or free variables, following the usual rules of static scoping in lambda-calculi.
The following table lists the reserved characters in Twelf.
All printing characters that are not reserved can be included in
identifiers, which are separated by whitespace or reserved characters.
In particular, A->B is an identifier, whereas A -> B
stands for the type of functions from A to B.
An uppercase identifier is one which begins with an underscore `_' or a letter in the range `A' through `Z'. A lowercase identifier begins with any other character except a reserved one. Numbers also count as lowercase identifiers and are not interpreted specially. Free variables in a declaration must be uppercase, bound variables and constants may be either uppercase or lowercase identifiers.
There are also four reserved identifiers with a predefined meaning which cannot be changed. Keep in mind that these can be constituents of other identifers which are not interpreted specially.
Constants have static scope, which means that they can be shadowed by
subsequent declarations. A shadowed identifier (which can no longer be
referred to in input) is printed as %id%. The printer for
terms renames bound variables so they do not shadow constants.
Free uppercase identifiers in declarations represent schematic variables. In order to distinguish them from other kinds of variables and constants they are printed as `'id' (backquote, followed by the identifer name) in error messages.
Go to the first, previous, next, last section, table of contents.