doc-src/Logics/CTT.tex
 changeset 153 0deb993885ce parent 114 96c627d2815e child 284 1072b18b2caa
--- a/doc-src/Logics/CTT.tex	Thu Nov 25 14:43:42 1993 +0100
+++ b/doc-src/Logics/CTT.tex	Thu Nov 25 15:15:53 1993 +0100
@@ -64,7 +64,7 @@
\begin{figure} \tabcolsep=1em  %wider spacing in tables
\begin{center}
\begin{tabular}{rrr}
-  \it symbol    & \it meta-type         & \it description \\
+  \it name      & \it meta-type         & \it description \\
\idx{Type}    & $t \to prop$          & judgement form \\
\idx{Eqtype}  & $[t,t]\to prop$       & judgement form\\
\idx{Elem}    & $[i, t]\to prop$      & judgement form\\
@@ -80,8 +80,8 @@
\idx{Sum}     & $[t, i\to t]\to t$    & general sum type\\
\idx{pair}    & $[i,i]\to i$          & constructor\\
\idx{split}   & $[i,[i,i]\to i]\to i$ & eliminator\\
-  \idx{fst} snd & $i\to i$              & projections\\[2ex]
-  \idx{inl} inr & $i\to i$              & constructors for $+$\\
+  \idx{fst} \idx{snd} & $i\to i$        & projections\\[2ex]
+  \idx{inl} \idx{inr} & $i\to i$        & constructors for $+$\\
\idx{when}    & $[i,i\to i, i\to i]\to i$    & eliminator for $+$\\[2ex]
\idx{Eq}      & $[t,i,i]\to t$        & equality type\\
\idx{eq}      & $i$                   & constructor\\[2ex]