%{ 
Some natural numbers; a demo of [[Project:Literate Twelf|Literate Twelf]]. 
}%
 
%{ == Syntax == }%
 
nat: type.
z : nat.
s : nat -> nat. 

%{ == Judgments == }%
 
%{ === Equality === }%
 
id-nat : nat -> nat -> type.
id-nat/refl : id-nat N N.
 
%{ === Addition === |}%
 
plus : nat -> nat -> nat -> type.
plus/z : plus z N N.
plus/s : plus N1 N2 N3 -> plus (s N1) N2 (s N3).

%{ Now we can see what it looks like to run a query: |check=decl}%

%solve _ : plus (s (s (s z))) (s (s z)) N.
 
%. 
 
This is a pretty boring presentation of the natural numbers;
it is roughly like all the other ones, like the article on [[natural numbers]].