From 7c65afbc934c1b46239bd25e0c8989f0012d9499 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 18 Aug 2024 13:31:08 -1000 Subject: [PATCH] Fix more line numbers Signed-off-by: Danila Fedorin --- content/blog/03_spa_agda_fixed_height.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/content/blog/03_spa_agda_fixed_height.md b/content/blog/03_spa_agda_fixed_height.md index 22aa140..bb9a987 100644 --- a/content/blog/03_spa_agda_fixed_height.md +++ b/content/blog/03_spa_agda_fixed_height.md @@ -192,7 +192,7 @@ three or more comparisons. Thus, the above-below lattice has a length of two comparisons (or alternatively, three elements). -{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 358 >}} +{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 363 >}} And that's it. @@ -300,7 +300,7 @@ Having decomposed the product chain into constituent chains, we simply combine the facts that they have to be bounded by the height of the `A` and `B` lattices, as well as the fact that they bound the combined chain. -{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 165 175 "hl_lines = 8-9" >}} +{{< codelines "agda" "agda-spa/Lattice/Prod.agda" 165 175 "hl_lines = 8-10" >}} This completes the proof! @@ -476,7 +476,7 @@ conversion functions, in both directions: With that, we can prove the second lattice's finite height: -{{< codelines "agda" "agda-spa/Isomorphism.agda" 66 73 >}} +{{< codelines "agda" "agda-spa/Isomorphism.agda" 66 80 >}} The conversion functions are also not too difficult to define. I give