We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent e967e02 commit 822982dCopy full SHA for 822982d
src/plfa/part1/Equality.lagda.md
@@ -285,8 +285,8 @@ if it improves readability!)
285
286
#### Exercise `trans` and `≡-Reasoning` (practice)
287
288
-Sadly, we cannot use the definition of `trans′` using ≡-Reasoning as the
289
-definition for trans. Can you see why? (Hint: look at the definition
+Sadly, we cannot use the definition of `trans′` using `≡-Reasoning` as the
+definition for `trans`. Can you see why? (Hint: look at the definition
290
of `_≡⟨_⟩_`)
291
292
```agda
0 commit comments