Skip to content

Commit 9638790

Browse files
negatratoronJefferson Carpenter
andauthored
Switch trans' from quote to prime in text to match agda code (#1081)
Co-authored-by: Jefferson Carpenter <jefferson@aoeu2code.com>
1 parent 6df65f9 commit 9638790

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/plfa/part1/Equality.lagda.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -285,7 +285,7 @@ if it improves readability!)
285285

286286
#### Exercise `trans` and `≡-Reasoning` (practice)
287287

288-
Sadly, we cannot use the definition of `trans'` using ≡-Reasoning as the
288+
Sadly, we cannot use the definition of `trans` using ≡-Reasoning as the
289289
definition for trans. Can you see why? (Hint: look at the definition
290290
of `_≡⟨_⟩_`)
291291

0 commit comments

Comments
 (0)