michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #23 from Fingerzam/fix-equation-in-quantifiers2

Browse source 
Fix typos in equations in Quantifiers.lagda
This commit is contained in:
wadler 2018-05-29 10:40:48 -03:00 committed by GitHub
commit 70a5ef7cbf
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Quantifiers.lagda
View file

@ -312,11 +312,11 @@ must show it is odd. We induct over the evidence of the existential,
and in the even case consider the two possibilities for the number and in the even case consider the two possibilities for the number
that is doubled. that is doubled.
- In the even case for `zero`, we must show `2 * zero` is even, which - In the even case for `zero`, we must show `zero * 2` is even, which
follows by `even-zero`. follows by `even-zero`.
- In the even case for `suc n`, we must show `2 * suc m` is even. The - In the even case for `suc n`, we must show `suc m * 2` is even. The
inductive hypothesis tells us that `1 + 2 * m` is odd, from which the inductive hypothesis tells us that `1 + m * 2` is odd, from which the
desired result follows by `even-suc`. desired result follows by `even-suc`.
- In the odd case, we must show `1 + m * 2` is odd. The inductive - In the odd case, we must show `1 + m * 2` is odd. The inductive