
%-------------------------------------------------------------------------------
% Uni-level                                                                     
%-------------------------------------------------------------------------------

\subsection{Uni-level representation}

Note that the rules for types and kinds are very similar.
Pfenning's experience with implementing Twelf is that if they
are separate much of the code has to be duplicated for
the two levels.  These concerns lead to the final 
grammar for Spine-Form LF, a single class of expressions for
terms, types, and kinds, classified by level.

$$
\begin{array}{llll}
\mathbf{Levels} & L & ::= & \Type \Spb \Kind \\
\mathbf{Expressions} & U & ::= & L \Spb \Pi(U_1,U_2) \Spb \lambda U \Spb H\cdot S \\
\mathbf{Heads} & H & ::= & c \Spb i\\
\mathbf{Spines} & S & ::= & \Nil \Spb U;S\\
\end{array} 
$$
