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

...
---

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 \\