From: Francesco Mazzoli <f@mazzo.li>
Date: Sun, 23 Jun 2013 14:00:56 +0000 (+0100)
Subject: ...
X-Git-Url: https://git.enpas.org/?p=bitonic-mengthesis.git;a=commitdiff_plain;h=1c05989bcb505bdf7ae2fcac6cbf02e3f3a24436

...
---

diff --git a/presentation.tex b/presentation.tex
index b0398e8..348340e 100644
--- a/presentation.tex
+++ b/presentation.tex
@@ -492,28 +492,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}