@@ -429,7 +429,7 @@ \subsection{Terms}
429429 \Dterm (\bits {0110} \cdot s) &= (s, \Error ) && \\
430430 \Dterm (\bits {0111} \cdot s) &= (s', \Builtin {b}) &&\quad \text {if } \Dbuiltin (s) = (s', b) \\
431431 \Dterm (\bits {1000} \cdot s) &= (s'', \Constr {i}{l}) &&\quad \text {if } \D _{\N }(s) = (s', i)\ \text {and}\ i < 2^{64} &&\ \text {and}\ \Dlist _{\mathsf {term}}(s') = (s'', l)\\
432- \Dterm (\bits {1001} \cdot s) &= (s', \Kase {u}{l}) &&\quad \text {if } \Dterm (s) = (s', u) &&\ \text {and}\ \Dlist _{\mathsf {term}}(s') = (s'', l)
432+ \Dterm (\bits {1001} \cdot s) &= (s'' , \Kase {u}{l}) &&\quad \text {if } \Dterm (s) = (s', u) &&\ \text {and}\ \Dlist _{\mathsf {term}}(s') = (s'', l)
433433\end {alignat* }
434434
435435\paragraph {NOTE. } The decoder $ \Dterm $ should fail if we are decoding a program
@@ -497,7 +497,7 @@ \subsection{Built-in types}
497497\begin {alignat* }{3}
498498 &\dtype (0 \cdot l) &&= (l, \ty {integer}) \\
499499 &\dtype (1 \cdot l) &&= (l, \ty {bytestring}) \\
500- &\dtype (2 \cdot l) &&= (l, \ty {string})) \\
500+ &\dtype (2 \cdot l) &&= (l, \ty {string}) \\
501501 &\dtype (3 \cdot l) &&= (l, \ty {unit}) \\
502502 &\dtype (4 \cdot l) &&= (l, \ty {bool}) \\
503503 &\dtype ([7,5] \cdot l) &&= (l', \listOf {t}) &&\quad \text {if $ \dtype (l) = (l', t)$ }\\
0 commit comments