- Will $\mytt : \myunit$ do as an argument? In other words, when type
- checking, do we have that
- \[
- \begin{array}{@{}c@{\ }c@{\ }c}
- \myunit & \mydefeq & \myfun{length} \myappsp \mylistt{3} \mathrel{\myfun{$>$}} 0 \\
- \myfun{length} \myappsp \mynil \mathrel{\myfun{$>$}} 0 & \mydefeq & \myempty \\
- (\myabs{\myb{x}\, \myb{y}}{\myb{y}}) \myappsp \myunit \myappsp \myappsp \mynat & \mydefeq & (\myabs{\myb{x}\, \myb{y}}{\myb{x}}) \myappsp \mynat \myappsp \myunit \\
- & \vdots &
- \end{array}
- \]
- ?
-\end{frame}
-
-\begin{frame}
- \frametitle{Definitional equality}
-
- The type checker needs a notion of equality between types.
-
- We reduce terms `as far as possible' (to their \emph{normal form}) and
- then compare them syntactically: