diff --git a/slides/ThProgUE10.pdf b/slides/ThProgUE10.pdf index df705ad..0e3fdc9 100644 Binary files a/slides/ThProgUE10.pdf and b/slides/ThProgUE10.pdf differ diff --git a/texfiles/slides10.tex b/texfiles/slides10.tex index 4631c71..246a3df 100644 --- a/texfiles/slides10.tex +++ b/texfiles/slides10.tex @@ -274,14 +274,14 @@ Leon Vatthauer} \end{lstlisting} In diesem Fall ergeben sich die folgenden ``Konstruktor-Funktionen'': \begin{lstlisting} - nil = $\lambda$ u f. u - cons = $\lambda$x l.$\lambda$ u f. f x (l u f) + nil = $\lambda$u f. u + cons = $\lambda$x l.$\lambda$u f. f x (l u f) \end{lstlisting} Für einen gegebenen (und durch \texttt{nil} und \texttt{cons} konstruierten) Term \texttt{t} des Typs \lstinline[keywords=List]|List a| verhält sich der Term '\lstinline|t u ($\lambda$x l. s)|' also genau so wie eine Funktion \texttt{f} für die für alle x (des Typs a) und alle l (des Typs \lstinline[keywords=List]|List a|) gilt: \begin{alignat*}{2} &f\;nil &&\rightarrow_{\beta\delta}^* u\\ - &f\;(cons\;x\;nil) &&\rightarrow_{\beta\delta}^* s[l \mapsto f\;l] + &f\;(cons\;x\;l) &&\rightarrow_{\beta\delta}^* s[l \mapsto f\;l] \end{alignat*} \vfill \begin{enumerate} @@ -300,8 +300,8 @@ Leon Vatthauer} \end{lstlisting} In diesem Fall ergeben sich die folgenden ``Konstruktor-Funktionen'': \begin{lstlisting} - nil = $\lambda$ u f. u - cons = $\lambda$x l.$\lambda$ u f. f x (l u f) + nil = $\lambda$u f. u + cons = $\lambda$x l.$\lambda$u f. f x (l u f) \end{lstlisting} \vfill \begin{enumerate}