diff options
author | Francesco Mazzoli <f@mazzo.li> | 2013-06-23 18:34:47 +0100 |
---|---|---|
committer | Francesco Mazzoli <f@mazzo.li> | 2013-06-23 18:34:47 +0100 |
commit | 4e064b0e81d5220dbdbae8af45a7bfdd3b373fa9 (patch) | |
tree | ae91f8aee353a90db34a89160d7307ed7948219a /presentation.tex | |
parent | 27d8348b35af1e7d5b2bc92e299f075f7b8de8e9 (diff) |
...
Diffstat (limited to 'presentation.tex')
-rw-r--r-- | presentation.tex | 14 |
1 files 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 \\ |