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

fix typo

Browse source
This commit is contained in:
Jeremy Siek 2020-03-30 15:57:23 -04:00
parent 8ffc49e929
commit 850de4b860
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/part3/Denotational.lagda.md
View file

@ -527,7 +527,7 @@ data Path : (n : ℕ) → Value → Set where
* A singleton path is of the form `f ↦ a ↦ a`.
* If there is a path from `a` to `b` and
an edge from `b` to `c` in graph of `f`,
an edge from `b` to `c` in the graph of `f`,
then there is a path from `a` to `c`.
This exercise is to prove that if `f ↦ a ↦ b` is a path of length `n`,