...

1 files changed, 7 insertions, 22 deletions

diff --git a/presentation.tex b/presentation.tex
index b0398e8..348340e 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -493,28 +493,6 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
 \end{frame}
 
 \begin{frame}
-  \frametitle{Records}
-  But also records:
-  \[
-  \mysyn{record}\ \mytyc{Tuple}\myappsp(\myb{A} : \mytyp)\myappsp(\myb{B} : \mytyp) \mapsto \mydc{tuple}\ \{ \myfun{fst} : \myb{A}, \myfun{snd} : \myb{B} \}
-  \]
-  Where each field defines a projection from instances of the record:
-  \[
-  \begin{array}{@{}l@{\ }c@{\ }l}
-    \myfun{fst} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{A} \\
-    \myfun{snd} & : & \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B} \myarr \myb{B}
-  \end{array}
-  \]
-  Where the projection's reduction rules are predictably
-  \[
-  \begin{array}{@{}l@{\ }l}
-    \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
-    \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
-  \end{array}
-  \]
-\end{frame}
-
-\begin{frame}
   \frametitle{Dependent defined types} \emph{Unlike} Haskell, we can
   have fields of a data constructor to depend on earlier fields:
   \[
@@ -532,6 +510,13 @@ Without the $\myb{l}$ we cannot compute, so we are stuck with
     \myfun{snd} & : (\myb{x} : \mytyc{Tuple}\myappsp\myb{A}\myappsp\myb{B}) \myarr \myb{B} \myappsp (\myfun{fst} \myappsp \myb{x})
   \end{array}
   \]
+  Where the projection's reduction rules are predictably
+  \[
+  \begin{array}{@{}l@{\ }l}
+    \myfun{fst}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmm \\
+    \myfun{snd}\myappsp&(\mydc{tuple}\myappsp\mytmm\myappsp\mytmn) \myred \mytmn \\
+  \end{array}
+  \]
 \end{frame}
 
 \begin{frame}