From 291d150c4bf650d2d73cefdd6b353c7af21ac4ad Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Sat, 31 Oct 2020 11:07:48 +0100
Subject: [PATCH] Fix typos
---
CHANGELOG.md | 2 +-
tex/derived.tex | 4 ++--
tex/program-logic.tex | 2 +-
theories/proofmode/classes.v | 2 +-
4 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1e91b7250..e2dfa3d07 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -406,7 +406,7 @@ Spies, and Tej Chajed. Thanks a lot to everyone involved!
* Make lemma `Excl_included` a bi-implication.
* Make `auth_update_core_id` work with any fraction of the authoritative
element.
-* Add `min_nat`, a RA for natural numbers with `min` as the operation.
+* Add `min_nat`, an RA for natural numbers with `min` as the operation.
* Add many missing `Proper`/non-expansiveness lemmas for maps and lists.
* Add `list_singletonM_included` and `list_lookup_singletonM_{lt,gt}` lemmas
about singletons in the list RA.
diff --git a/tex/derived.tex b/tex/derived.tex
index 119a24fa9..24b5e7d4a 100644
--- a/tex/derived.tex
+++ b/tex/derived.tex
@@ -91,11 +91,11 @@ from which we can derive
\subsection{Boxes}
-The idea behind the \emph{boxes} is to have an proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
+The idea behind the \emph{boxes} is to have a proposition $\prop$ that is actually split into a number of pieces, each of which can be taken out and back in separately.
In some sense, this is a replacement for having an ``authoritative PCM of Iris propositions itself''.
It is similar to the pattern involving saved propositions that was used for the barrier~\cite{iris2}, but more complicated because there are some operations that we want to perform without a later.
-Roughly, the idea is that a \emph{box} is a container for an proposition $\prop$.
+Roughly, the idea is that a \emph{box} is a container for a proposition $\prop$.
A box consists of a bunch of \emph{slices} which decompose $\prop$ into a separating conjunction of the propositions $\propB_\sname$ governed by the individual slices.
Each slice is either \emph{full} (it right now contains $\propB_\sname$), or \emph{empty} (it does not contain anything currently).
The proposition governing the box keeps track of the state of all the slices that make up the box.
diff --git a/tex/program-logic.tex b/tex/program-logic.tex
index 557c8c64d..5404f6582 100644
--- a/tex/program-logic.tex
+++ b/tex/program-logic.tex
@@ -23,7 +23,7 @@ We assume to have the following four cameras available:
\end{align*}
The last two are the tokens used for managing invariants, $\textdom{Inv}$ is the monoid used to manage the invariants themselves.
-We assume that at the beginning of the verification, instances named $\gname_{\textdom{State}}$, $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
+We assume that at the beginning of the verification, instances named $\gname_{\textdom{Inv}}$, $\gname_{\textdom{En}}$ and $\gname_{\textdom{Dis}}$ of these cameras have been created, such that these names are globally known.
\paragraph{World Satisfaction.}
We can now define the proposition $W$ (\emph{world satisfaction}) which ensures that the enabled invariants are actually maintained:
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 50f03e157..9c1d7af95 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -308,7 +308,7 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
The reason for this is that if given an evar, these typeclasses
would typically try to instantiate this evar with some arbitrary
- logical constructs such as emp or True. Therefore, we use an Hint
+ logical constructs such as emp or True. Therefore, we use a Hint
Mode to disable all the instances that would have this behavior. *)
Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
make_embed : ⎡P⎤ ⊣⊢ Q.
--
GitLab