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