| Simple Sorts | nat : type | %sort nat | data nat : Set where ... | |
| Constructors | zero : nat | %term zero nat | zero : nat | Flag to allow for colon in STELF |
| Constructors with params | succ : nat -> nat | %term succ %-> nat nat | succ : nat -> nat | Flag allows for writing %-> as old infix -> |
| Reversed | succ : nat <- nat | %term succ %<- nat nat | None | See above |
| Simply indexed sorts | add : nat -> nat -> nat -> type | %sort add nat nat nat | data add : Nat -> Nat -> Nat -> Set | |
| Complete indexed sorts | eq : {T : tp} (tm T -> tm T -> type) | %sort eq {T type} (tm T) (tm T) | data eq (T : tp) : tm T -> tm T -> Set | type valid ident in STELF |
| Dependent function types | {X : T} U | {X T} U | (X : T) -> U | |
| Explicit Implicits | None | {{A B C}} X | forall {A} -> forall {B} -> forall {C} -> X | STELF’s must not have a sort |
| Multiple binders (dependent functions) | None | {(X Y Z) T} U | (X Y Z : T) -> U | |
| Omitted type | {X} or {X : _} | {X} or {X _} | forall X | |
