From 4aca0dd41eaef0005694e2158ffc4bc4a31531a3 Mon Sep 17 00:00:00 2001
From: Ben Siraphob <bensiraphob@gmail.com>
Date: Wed, 14 Jul 2021 20:16:05 +0700
Subject: [PATCH] Minor wording adjustments

---
 tex/chHierarchy.tex     | 9 ++++-----
 tex/chSigmaBool.tex     | 6 +++---
 tex/chTypeInference.tex | 8 ++++----
 3 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/tex/chHierarchy.tex b/tex/chHierarchy.tex
index 05b82462..3d2b88fe 100644
--- a/tex/chHierarchy.tex
+++ b/tex/chHierarchy.tex
@@ -263,7 +263,7 @@ \section{Structure interface}\label{str:itf}
 structure instance. This means that \lstinline/'I_p/ should also have
 an instance of the \C{finRingType} join structure (for \C{p} of the
 right shape). This is not automatic, but thanks to the cloning
-constructor requires only one line in \lib{zmodp}.
+constructor it requires only one line in \lib{zmodp}.
 
 \begin{coq}{name=zp8}{}
 Canonical Zp_finRingType := [finRingType of 'I_p].
@@ -539,8 +539,8 @@ \section{Packed classes}\label{sec:packed}
 defined using the \C{find} operator provided by the interface, and its
 properties follow from the axiom of countable choice. Indeed, although
 the choice axiom is not provable in general in \mcbCIC{}, its
-restriction to countable type can be proved.
-which is derivable in \mcbCIC{}% \footnote{behind the
+restriction to countable types is provable.
+% \footnote{behind the
 % \C{\{m|..\}} notation lies the \C{sig} dependent pair.  Such an inductive
 % data type is a copy of the existential quantifier but is
 % declared as a data type rather than a
@@ -549,7 +549,6 @@ \section{Packed classes}\label{sec:packed}
 % the existential witness \C{n}.  In other words the proof in
 % input is only used to justify the termination of the
 % search for \C{m}.}
-.
 
 \begin{coq}{}{}
 Lemma find_ex_minn (P : pred nat)  :
@@ -976,7 +975,7 @@ \section{Linking a custom data type to the library}
 
 The sub-type kit of chapter~\ref{ch:sigmabool} is not the only
 way to easily add instances to the library.  For example
-imagine we are interested to define the type of a wind rose and attach
+imagine we are interested in defining the type of a wind rose and attach
 to it the theory of finite types.
 
 \begin{coq}{}{}
diff --git a/tex/chSigmaBool.tex b/tex/chSigmaBool.tex
index b9510619..52d02124 100644
--- a/tex/chSigmaBool.tex
+++ b/tex/chSigmaBool.tex
@@ -569,15 +569,15 @@ \section{Finite types and their theory}
 
 \begin{coq}{name=fintype}{title=Interface for finite types}
 Notation count_mem x := (count [pred y | y == x]).
-Module finite.
+Module Finite.
 Definition axiom (T : eqType) (e : seq T) :=
   forall x : T, count_mem x e = 1.
 
 Record mixin_of (T : eqType) := Mixin {
   enum : seq T;
-  _ : axiom T enum;
+  _ : axiom enum;
 }
-End finite.
+End Finite.
 \end{coq}
 
 The axiom asserts that any inhabitant of \C{T} occurs exactly once
diff --git a/tex/chTypeInference.tex b/tex/chTypeInference.tex
index 4dc03fa2..7cb2219d 100644
--- a/tex/chTypeInference.tex
+++ b/tex/chTypeInference.tex
@@ -1509,7 +1509,7 @@ \subsection{Assumptions of a bigop lemma}\label{sec:bigoplemmas}
 \end{coq}
 \coqrun{name=uniqp2}{ssr,bigop}
 
-If we print such statement once the \C{Section MonoidProperties} is
+If we print such a statement once the \C{Section MonoidProperties} is
 closed, we see the requirement affecting the operation \C{op} explicitly.
 
 \begin{coqout}{}{}
@@ -1523,7 +1523,7 @@ \subsection{Assumptions of a bigop lemma}\label{sec:bigoplemmas}
 Note that wherever the operation \C{op} occurs, we also find
 the \C{Monoid.operator} projection.
 
-To make this lemma available on the addition on natural numbers,
+To make this lemma available for addition on natural numbers,
 we need to declare the canonical monoid structure on \C{addn}.
 
 \begin{coq}{name=natmonoid}{}
@@ -1596,7 +1596,7 @@ \subsection{Searching the bigop library}
 "big"};  index exchange lemmas with \C{ Search "exchange" "big"};
 lemmas pulling out elements from the iteration
 with \C{ Search "rec" "big"}; lemmas  working on the filter condition
-with \C{ Search "cond" "big"}, etc\ldots
+with \C{ Search "cond" "big"}, and so on.
 
 
 Finally the \mcbMC{} user is advised to read the contents of the
@@ -1633,7 +1633,7 @@ \section{Stable notations for big operators}
 \end{coq}
 
 To solve these problems we craft a box, \C{BigBody}, with
-separate compartments for each sub component.  Such box will
+separate compartments for each sub component.  Such a box will
 be used under a single binder and will hold an occurrence of the
 bound variable even if it is unused in the predicate and in the
 general term.