Comparing Syntax

Syntax Comaprison

Feature	Twelf	STELF	Agda	Notes
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`