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

Merge pull request #465 from MatthiasGabriel/patch-2

Browse source 
Remove strange line break
This commit is contained in:
Wen Kokke 2020-02-13 14:48:58 +00:00 committed by GitHub
commit a8b53353a7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part1/Induction.lagda.md
View file

@ -656,8 +656,8 @@ time we are concerned with judgments asserting associativity:
Now, we apply the rules to all the judgments we know about. The base
case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural
`n` and `p`. The inductive case tells us that if `(m + n) + p ≡ m +
(n + p)` (on the day before today) then
`n` and `p`. The inductive case tells us that if
`(m + n) + p ≡ m + (n + p)` (on the day before today) then
`(suc m + n) + p ≡ suc m + (n + p)` (today).
We didn't know any judgments about associativity before today, so that
rule doesn't give us any new judgments: