From c607913898bf610a0dd764889bd5dd954a0125be Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Wed, 15 Apr 2020 09:48:24 -0400
Subject: [PATCH] Typo in translation rule

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

diff --git a/frap_book.tex b/frap_book.tex
index 86b7800..726f488 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -4079,7 +4079,7 @@ We will define a judgment $\dscomp{v}{c}{s}$, indicating that mixed-embedded com
 
 A good warmup is defining a related judgment $\dscomp{v}{n}{e}$, compiling normal Gallina numeric expressions $n$ into syntactic expressions $e$.
 
-$$\infer{\dscomp{v}{x}{n}}{
+$$\infer{\dscomp{v}{n}{x}}{
   v(x) = n
 }
 \quad \infer{\dscomp{v}{n_1 + n_2}{e_1 + e_2}}{