summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-11-17 07:54:59 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2013-11-17 07:54:59 -0500
commit1f1fc5c83dae5167133a56ecae33692a0d6444db (patch)
tree70fee330ce7b7c0b3d4b7cf7246ded4aa19cb348 /doc
parent4259d248050c93180767c076469431f11b8fe984 (diff)
Manual: add a pointer to background reading on inference rule notation
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex5
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 41b5f952..ac12c3b7 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -619,6 +619,11 @@ A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Bas
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.