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

Fix typos in equations in Quantifiers.lagda

Browse source
This commit is contained in:
Juhana Laurinharju 2018-05-27 21:53:24 +03:00
parent 246c2b3287
commit ea4d75c36b
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