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

fix formatting

Browse source
This commit is contained in:
Jeremy Siek 2020-03-30 16:21:48 -04:00
parent 2412de33fc
commit 14b1fb0e10
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/part3/Compositional.lagda.md
View file

@ -66,8 +66,8 @@ rules `↦-intro`, `⊥-intro`, and `⊔-intro`.
If one squints hard enough, the `ℱ` function starts to look like the
`curry` operation familar to functional programmers. It turns a
function that expects a tuple of length `n + 1` (the environment `Γ ,
★`) into a function that expects a tuple of length `n` and returns a
function that expects a tuple of length `n + 1` (the environment `Γ , ★`)
into a function that expects a tuple of length `n` and returns a
function of one parameter.
Using this `ℱ`, we hope to prove that