From a6624bdcf28faaf8dd5642d88cf91bbcaa320f71 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Tue, 18 Apr 2017 21:01:12 -0400
Subject: [PATCH] Typo fix in book

---
 frap_book.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/frap_book.tex b/frap_book.tex
index b2054d8..690790e 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -3277,7 +3277,7 @@ $$\infer{\hoare{P}{\ifte{b}{c_1}{c_2}}{\lambda s. \; Q_1(s) \lor Q_2(s)}}{
   & \hoare{\lambda s. \; P(s) \land \neg \denote{b}(s)}{c_2}{Q_2}
 }$$
 
-Coming to loops, we at least have a purpose for the assertion annotated on each one.
+Coming to loops, we at last have a purpose for the assertion annotated on each one.
 \invariants
 We call those assertions \emph{loop invariants}\index{loop invariants}; one of these is meant to be true every time a loop iteration begins.
 We will try to avoid confusion with the more fundamental concept of invariant for transition systems, though in fact the two are closely related formally, which we will see in the last section of this chapter.