From 850de4b860e960a4448d7a7a82ff1993e9e7a261 Mon Sep 17 00:00:00 2001 From: Jeremy Siek Date: Mon, 30 Mar 2020 15:57:23 -0400 Subject: [PATCH] fix typo --- src/plfa/part3/Denotational.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md index 359611dc..fe4ddaf7 100644 --- a/src/plfa/part3/Denotational.lagda.md +++ b/src/plfa/part3/Denotational.lagda.md @@ -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`,