git.iko.soy/Idris-dev
on e4cefe8 help sign in
Idris-dev/impl-paper/typechecking.tex
18 lines 416 B history raw
1\section{The Core Type Theory}
3\DM{
4\begin{array}{rll@{\hg}|rll}
5\vt ::= & \Type_i & (\mbox{type universes}) &
6\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\
8 \mid & \vx & (\mbox{variable}) &
9 \mid & \LET\:\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\
11 \mid & \vb\SC\:\vt & (\mbox{binding}) &
12 \mid & \all{\vx}{\vt} & (\mbox{function space}) \\
14 \mid & \vt\:\vt & (\mbox{application})
16\end{array}