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

Fix break verbatim

Browse source
This commit is contained in:
Jonathan Prieto-Cubides 2018-07-06 00:43:04 +02:00 committed by GitHub
parent e42aa017da
commit 504b194db2
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/plfa/Induction.lagda
View file

@ -497,9 +497,10 @@ time we are concerned with judgements asserting associativity.
Now, we apply the rules to all the judgements we know about. The base Now, we apply the rules to all the judgements we know about. The base
case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural 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` 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 (n + p)` (on the day before today) then
+ p)` (today). We didn't know any judgments about associativity `(suc m + n) + p ≡ suc m + (n + p)` (today).
before today, so that rule doesn't give us any new judgments. We didn't know any judgments about associativity before today, so that
rule doesn't give us any new judgments.
-- on the first day, we know about associativity of 0 -- on the first day, we know about associativity of 0
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ... (0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...