# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1384692899 18000
# Node ID 779c390382b91736cbf8f3e8e2a5bf2c63bb0f93
# Parent  abb0e95dcaa1be37273a4854fa71f7fd4362f2ba
Manual: add a pointer to background reading on inference rule notation

diff -r abb0e95dcaa1 -r 779c390382b9 doc/manual.tex
--- a/doc/manual.tex	Thu Nov 14 06:36:36 2013 -0500
+++ b/doc/manual.tex	Sun Nov 17 07:54:59 2013 -0500
@@ -619,6 +619,11 @@
 
 In this section, we give a declarative presentation of Ur's typing rules and related judgments.  Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values.
 
+The notations used here are the standard ones of programming language semantics.  They are probably the most effective way to convey this information.  At the same time, most Ur/Web users can probably get by \emph{without} knowing the contents of this section!  If you're interested in diving into the details of Ur typing but are unfamiliar with ``inference rule notation,'' I recommend the following book:
+\begin{quote}
+  Benjamin C. Pierce, \emph{Types and Programming Languages}, MIT Press, 2002.
+\end{quote}
+
 Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules.  We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed.
 \begin{itemize}
 \item $\Gamma \vdash \kappa$ expresses kind well-formedness.