From 78e792e83d966b8ab7c1955f057fc9e3725f4a2c Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 1 Mar 2021 17:55:28 -0500 Subject: [PATCH] Fix typos --- frap_book.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/frap_book.tex b/frap_book.tex index 675e4a2..f4410e5 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -977,7 +977,7 @@ Specifically, when we defined $P$ inductively and want to conclude $Q$ from it, We transform each rule into one obligation within the induction, by replacing $P$ with $Q$ in the conclusion, in addition to taking each premise $P(e)$ and pairing it with a new premise $Q(e)$ (an \emph{induction hypothesis}\index{induction hypothesis}). Our example of $\mathsf{favorites}$ is a degenerate inductive definition whose principle requires no induction hypotheses. Thus, to prove $\forall x. \; \favs{x} \Rightarrow Q(x)$, we must establish the following. -$$\infer{Q(7)}{} +$$\infer{Q(17)}{} \quad \infer{Q(23)}{} \quad \infer{Q(42)}{}$$ @@ -1206,7 +1206,7 @@ $$\infer{\Gamma \vdash \top}{} \quad \infer{\Gamma \vdash \phi_1 \lor \phi_2}{ \Gamma \vdash \phi_1 } -\quad \infer{\vdash \phi_1 \lor \phi_2}{ +\quad \infer{\Gamma \vdash \phi_1 \lor \phi_2}{ \Gamma \vdash \phi_2 }$$