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

Fix typo in an equation in quantifiers

Browse source
This commit is contained in:
Juhana Laurinharju 2018-05-27 21:41:23 +03:00
parent 246c2b3287
commit 3ee374bb0d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Quantifiers.lagda
View file

@ -291,7 +291,7 @@ substituting for `n`.
- If the number is odd because it is the successor of an even number,
then we apply the induction hypothesis to give a number `m` and
evidence that `m * 2 ≡ n`. We return a pair consisting of `suc m` and
evidence that `1 + 2 * m = suc n`, which is immediate after
evidence that `1 + m * 2 ≡ suc n`, which is immediate after
substituting for `n`.
This completes the proof in the forward direction.