|
|
@ -6333,7 +6333,7 @@ that allow us to redefine the target of $\Write$ operations locally. |
|
|
\ba[t]{@{}l} |
|
|
\ba[t]{@{}l} |
|
|
\Let\;ino \revto \Case\;\Do\;\UCreate~fname\;\{ |
|
|
\Let\;ino \revto \Case\;\Do\;\UCreate~fname\;\{ |
|
|
\ba[t]{@{~}l@{~}c@{~}l} |
|
|
\ba[t]{@{~}l@{~}c@{~}l} |
|
|
\None &\mapsto& \exit\,1\\ |
|
|
|
|
|
|
|
|
\None &\mapsto& \exit~1\\ |
|
|
\Some~ino &\mapsto& ino\} |
|
|
\Some~ino &\mapsto& ino\} |
|
|
\ea\\ |
|
|
\ea\\ |
|
|
\In\;\Handle\;m\,\Unit\;\With\\ |
|
|
\In\;\Handle\;m\,\Unit\;\With\\ |
|
|
|
