From 93ef5add7a69eb8aacb5eacd37f91a5c4e104251 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Mon, 4 Mar 2019 11:28:37 -0500
Subject: [PATCH] Closes #28

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

diff --git a/frap_book.tex b/frap_book.tex
index 5412798..081d499 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -1972,6 +1972,7 @@ One example, which we'll formalize in more detail shortly, would be to label eac
 \renewcommand{\O}[0]{\mathsf{O}}
 
 As an example, consider this formalization of even-odd analysis, whose proof of soundness is left as an exercise for the reader.
+(While the treatment of subtraction may seem gratuitously imprecise, recall that we are working here with natural numbers and not integers, such that subtraction ``sticks'' at zero when the result would otherwise be negative.)
 \begin{eqnarray*}
   \mathbb D &=& \{\E, \O, \top\} \\
   \mathcal C(n) &=& \textrm{$\E$ or $\O$, depending on parity of $n$} \\