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

More: fixes an informal definition of swap×

Browse source
This commit is contained in:
Marko Dimjašević 2020-10-14 18:12:16 +02:00
parent 20516d9e8e
commit ea1b9c2150
No known key found for this signature in database
GPG key ID: 565EE9641503F0AA
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/plfa/part2/More.lagda.md
View file

@ -206,7 +206,7 @@ construct to a calculus without the construct.
Here is a function to swap the components of a pair: Here is a function to swap the components of a pair:
swap× : ∅ ⊢ A `× B ⇒ B `× A swap× : ∅ ⊢ A `× B ⇒ B `× A
swap× = ƛ z ⇒ `⟨ proj₂ z , proj₁ z ⟩ swap× = ƛ z ⇒ `⟨ `proj₂ z , `proj₁ z ⟩
## Alternative formulation of products ## Alternative formulation of products