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

Merge pull request #188 from mdimjasevic/conn-10

Browse source 
Connectives: fixes the text of exercises to match names of proofs
This commit is contained in:
Philip Wadler 2019-01-31 09:44:06 -02:00 committed by GitHub
commit 1c93405eee
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/Connectives.lagda
View file

@ -491,7 +491,7 @@ is the identity of sums _up to isomorphism_.
#### Exercise `⊥-identityˡ` (recommended)
Show zero is the left identity of addition.
Show empty is the left identity of sums up to isomorphism.
\begin{code}
-- Your code goes here
@ -499,7 +499,7 @@ Show zero is the left identity of addition.
#### Exercise `⊥-identityʳ`
Show zero is the right identity of addition.
Show empty is the right identity of sums up to isomorphism.
\begin{code}
-- Your code goes here