Fixed typos
This commit is contained in:
parent
3fa889d223
commit
ef90555a1d
2 changed files with 5 additions and 5 deletions
Binary file not shown.
|
@ -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}
|
||||
|
|
Loading…
Reference in a new issue