From a38bdbac8c0e48eba4c7f942a6e1b4cc3d2b0793 Mon Sep 17 00:00:00 2001 From: 0xd34df00d <0xd34df00d@gmail.com> Date: Sat, 24 Oct 2020 10:01:56 -0500 Subject: [PATCH] Fix a tiny rendering bug due to a \n in inline code (#536) --- src/plfa/part1/Relations.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 5263b14a..8d6f6bdb 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -334,8 +334,8 @@ using holes and the `C-c C-c`, `C-c C-,`, and `C-c C-r` commands. ## Anti-symmetry The third property to prove about comparison is that it is -antisymmetric: for all naturals `m` and `n`, if both `m ≤ n` and `n ≤ -m` hold, then `m ≡ n` holds: +antisymmetric: for all naturals `m` and `n`, if both `m ≤ n` and +`n ≤ m` hold, then `m ≡ n` holds: ``` ≤-antisym : ∀ {m n : ℕ} → m ≤ n