...

diff --git a/presentation.tex b/presentation.tex
index 348340e3d3f5dd566d8e80049d86fccc91e532f5..22e619ab600e6e51616670eea520b8469ab7ca26 100644 (file)
--- a/presentation.tex
+++ b/presentation.tex
@@ -295,8 +295,7 @@
   \[
   \begin{array}{@{}l@{\ }l@{\ \ \ }l}
     \mysyn{data}\ \myempty & & \text{No members.} \\
-    \mysyn{data}\ \myunit  & = \mytt & \text{One member.} \\
-    \mysyn{data}\ \mynat   & = \mydc{zero} \mydcsep \mydc{suc}\myappsp\mynat & \text{Natural numbers.}
+    \mysyn{data}\ \myunit  & \mapsto \mytt & \text{One member.}
   \end{array}
   \]
   $\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
@@ -312,9 +311,16 @@
 
 \begin{frame}
   \frametitle{Theorem provers, dependent types}
-  % TODO examples first
+  \[ \mysyn{data}\ \mylist{\myb{A}} \mapsto \mynil \mydcsep \myb{A} \mycons \mylist{\myb{A}} \]
+  We want to express a `non-emptiness' property for lists:
+  \[
+  \begin{array}{@{}l@{\myappsp}c@{\ }l}
+    \myfun{non-empty} : \mylist{\myb{A}} \myarr \mytyp \\
+    \myfun{non-empty} & \mynil & = \myempty \\
+    \myfun{non-empty} & (\myb{x} \mycons \myb{l}) & = \myunit
+  \end{array}
+  \]
 
-  We can express relations:
   \[
   \begin{array}{@{}l}
     (\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\