Expressions

New

One of the largest differences between Twelf and STELF syntax is the syntax of expressions. STELF aims to have a simple syntax, almost akin to the syntax of Metamath or Z3, while still being able to express concepts consicsly. It was also designed to be easy to parse, and easy to debug. Almost every expresion in STELF starts with a literal token, thus making figuring out what was intended easier.

Unrestricted Syntax

A number of syntax constructs lose their restrictions in STELF. Per as a matter of fact, the only things that are special in expressions are whitespace, and any of %_()[]{}. Every other charecter is treated as a single token, without any sets of tokens being important.

The following syntax constructs are removed in STELF:

1. -> and <- are both removed
2. = is no longer a special token (strictly, = wasn’t a token in an expression)
3. : is removed (ie, X : A)
4. type is removed
5. +*-1 are all removed (mode expressions specifically)

Introduction Syntax

The syntaxes of $\lambda$ and $\Pi$ are simplified in STELF. Namely, the new declerations syntax is used for both

Arrow Chains

One of the largest differences between Twelf and STELF is the arrow syntax. In Twelf, one can write A -> B -> C to mean {_ : A} {_ : B} C. In STELF, there are two ways we can do this:

1. Write this out in full. This isn’t as bad as it seems, {_ A} {_ B} C contains only two more charecters then A -> B -> C, (the 2 _) and is much more explicit. However, this fails for the Prolog-esque <- syntax, which is why we have a second option:

2. The new arrow chain syntax. This differs from the old syntax in two main ways:

   • -> is replaced with %->, and %<-