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

small fix to Connectives

Browse source
This commit is contained in:
wadler 2021-06-26 15:43:48 +01:00
parent e54f752b6f
commit 00a04e43d1
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/Connectives.lagda.md
View file

@ -58,8 +58,8 @@ Evidence that `A × B` holds is of the form `⟨ M , N ⟩`, where `M`
provides evidence that `A` holds and `N` provides evidence that `B` provides evidence that `A` holds and `N` provides evidence that `B`
holds. holds.
Given evidence that `A × B` holds, we can conclude that either Given evidence that `A × B` holds, we can conclude that both
`A` holds or `B` holds: `A` holds and `B` holds:
``` ```
proj₁ : ∀ {A B : Set} proj₁ : ∀ {A B : Set}
→ A × B → A × B