projects
/
bitonic-mengthesis.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
27d8348
)
...
author
Francesco Mazzoli
<f@mazzo.li>
Sun, 23 Jun 2013 17:34:47 +0000
(18:34 +0100)
committer
Francesco Mazzoli
<f@mazzo.li>
Sun, 23 Jun 2013 17:34:47 +0000
(18:34 +0100)
presentation.tex
patch
|
blob
|
history
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.} \\
\[
\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$.
\end{array}
\]
$\myempty : \mytyp$, $\myunit : \mytyp$, $\mynat : \mytyp$.
@@
-312,9
+311,16
@@
\begin{frame}
\frametitle{Theorem provers, dependent types}
\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 \\
\[
\begin{array}{@{}l}
(\myfun{${>}$}) : \mynat \myarr \mynat \myarr \mytyp \\