pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix typos

Browse source
This commit is contained in:
Adam Chlipala 2021-03-01 17:55:28 -05:00
parent 4fdc85ae5c
commit 78e792e83d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
frap_book.tex
View file

@ -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}). 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. 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(23)}{}
\quad \infer{Q(42)}{}$$ \quad \infer{Q(42)}{}$$
@ -1206,7 +1206,7 @@ $$\infer{\Gamma \vdash \top}{}
\quad \infer{\Gamma \vdash \phi_1 \lor \phi_2}{ \quad \infer{\Gamma \vdash \phi_1 \lor \phi_2}{
\Gamma \vdash \phi_1 \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 \Gamma \vdash \phi_2
}$$ }$$