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

Remove strange line break

Browse source 
Remove a strange line break in the middle of the formula. I guess the mark-down respects that line break because it's part of the formula.
This commit is contained in:
Matthias Gabriel 2020-02-13 15:46:39 +01:00 committed by GitHub
parent 10bfcebc44
commit 747998cd63
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: