copy edit index

book.tex

@@ -776,7 +776,7 @@ programs in the language. Instead we write down a set of rules, a
 define the concrete syntax of a language, but they can also be used to
 describe the abstract syntax. We write our rules in a variant of
 Backus-Naur form (BNF)~\citep{Backus:1960aa,Knuth:1964aa}.
-\index{subject}{Backus-Naur Form}\index{subject}{BNF} As an example,
+\index{subject}{Backus-Naur form}\index{subject}{BNF} As an example,
 we describe a small language, named \LangInt{}, that consists of
 integers and arithmetic operations.  \index{subject}{grammar}
 
@@ -10374,7 +10374,7 @@ The Kleene fixed-point theorem states that if a function $f$ is
 monotone (better inputs produce better outputs), then the least fixed
 point of $f$ is the least upper bound of the \emph{ascending Kleene
   chain} obtained by starting at $\bot$ and iterating $f$, as
-follows:\index{subject}{Kleene Fixed-Point Theorem}
+follows:\index{subject}{Kleene fixed-point theorem}
 \[
 \bot \sqsubseteq f(\bot) \sqsubseteq f(f(\bot)) \sqsubseteq \cdots
   \sqsubseteq f^n(\bot) \sqsubseteq \cdots
@@ -11370,7 +11370,7 @@ To create the s-expression for the \code{Vector} type in
 figure~\ref{fig:type-check-Lvec}, we use the
 \href{https://docs.racket-lang.org/reference/quasiquote.html}{unquote-splicing
   operator} \code{,@} to insert the list \code{t*} without its usual
-start and end parentheses. \index{subject}{unquote-slicing}}
+start and end parentheses. \index{subject}{unquote-splicing}}
 %
 \python{records the type of each tuple expression in a new field
   named \code{has\_type}. Because the type checker has to compute the type