Fix more line numbers
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
fb071e55aa
commit
7c65afbc93
|
@ -192,7 +192,7 @@ three or more comparisons.
|
||||||
Thus, the above-below lattice has a length of two comparisons (or alternatively,
|
Thus, the above-below lattice has a length of two comparisons (or alternatively,
|
||||||
three elements).
|
three elements).
|
||||||
|
|
||||||
{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 358 >}}
|
{{< codelines "agda" "agda-spa/Lattice/AboveBelow.agda" 357 363 >}}
|
||||||
|
|
||||||
And that's it.
|
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,
|
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.
|
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!
|
This completes the proof!
|
||||||
|
|
||||||
|
@ -476,7 +476,7 @@ conversion functions, in both directions:
|
||||||
|
|
||||||
With that, we can prove the second lattice's finite height:
|
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
|
The conversion functions are also not too difficult to define. I give
|
||||||
|
|
Loading…
Reference in New Issue
Block a user