From 4e064b0e81d5220dbdbae8af45a7bfdd3b373fa9 Mon Sep 17 00:00:00 2001
From: Francesco Mazzoli <f@mazzo.li>
Date: Sun, 23 Jun 2013 18:34:47 +0100
Subject: [PATCH] ...

---
 presentation.tex | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/presentation.tex b/presentation.tex
index 348340e..22e619a 100644
--- 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 \\
-- 
2.30.2