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

[ Induction ] Fix typo

Browse source 
of of typo
This commit is contained in:
Jonathan Prieto-Cubides 2018-07-06 00:11:44 +02:00 committed by GitHub
parent d9b0872a66
commit e42aa017da
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/Induction.lagda
View file

@ -314,7 +314,7 @@ For the base case, we must show:
zero + zero ≡ zero zero + zero ≡ zero
Simplifying with the base case of of addition, this is straightforward. Simplifying with the base case of addition, this is straightforward.
For the inductive case, we must show: For the inductive case, we must show:
@ -385,7 +385,7 @@ For the base case, we must show:
zero + suc n ≡ suc (zero + n) zero + suc n ≡ suc (zero + n)
Simplifying with the base case of of addition, this is straightforward. Simplifying with the base case of addition, this is straightforward.
For the inductive case, we must show: For the inductive case, we must show: