Skip to content

Minor wording adjustments #136

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gares merged 1 commit into from
Jul 14, 2021
Merged

Minor wording adjustments #136

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions tex/chHierarchy.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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].
Expand Down Expand Up @@ -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
Expand All @@ -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) :
Expand Down Expand Up @@ -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}{}{}
Expand Down
6 changes: 3 additions & 3 deletions tex/chSigmaBool.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions tex/chTypeInference.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}{}{}
Expand All @@ -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}{}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down