From 59fdaa208b834ab2e6e23262405d0e9f4559e9aa Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 18 Feb 2012 08:14:51 -0500
Subject: Update manual to fix lexical table and clarify sequencing notation

---
 doc/manual.tex | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'doc/manual.tex')

diff --git a/doc/manual.tex b/doc/manual.tex
index db24953a..169560f1 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -348,7 +348,7 @@ We give the Ur language definition in \LaTeX $\;$ math mode, since that is prett
   \begin{tabular}{rl}
     \textbf{\LaTeX} & \textbf{ASCII} \\
     $\to$ & \cd{->} \\
-    $\longrightarrow$ & \cd{-->} \\
+    $\longrightarrow$ & \cd{-{}->} \\
     $\times$ & \cd{*} \\
     $\lambda$ & \cd{fn} \\
     $\Rightarrow$ & \cd{=>} \\
@@ -548,6 +548,8 @@ The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]
 
 A tuple type $\tau_1 \times \ldots \times \tau_n$ expands to a record type $\{1 : \tau_1, \ldots, n : \tau_n\}$, with natural numbers as field names.  A tuple expression $(e_1, \ldots, e_n)$ expands to a record expression $\{1 = e_1, \ldots, n = e_n\}$.  A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$.  Positive natural numbers may be used in most places where field names would be allowed.
 
+The syntax $()$ expands to $\{\}$ as a pattern or expression.
+
 In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards.  More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
 
 Further, the signature item or declaration syntax $\mt{con} \; x \; b^+ = c$ is shorthand for wrapping of the appropriate $\lambda$s around the righthand side $c$.  The $b$ elements may not include $X$, and there may also be an optional $:: \kappa$ before the $=$.
@@ -1393,7 +1395,7 @@ $$\begin{array}{l}
   \hspace{.1in} \to \mt{monad} \; \mt{m}
 \end{array}$$
 
-The Ur/Web compiler provides syntactic sugar for monads, similar to Haskell's \cd{do} notation.  An expression $x \leftarrow e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda x \Rightarrow e_2)$, and an expression $e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda () \Rightarrow e_2)$.
+The Ur/Web compiler provides syntactic sugar for monads, similar to Haskell's \cd{do} notation.  An expression $x \leftarrow e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda x \Rightarrow e_2)$, and an expression $e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda () \Rightarrow e_2)$.  Note a difference from Haskell: as the $e_1; e_2$ case desugaring involves a function with $()$ as its formal argument, the type of $e_1$ must be of the form $m \; \{\}$, rather than some arbitrary $m \; t$.
 
 \subsection{Transactions}
 
-- 
cgit v1.2.3