Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Write more

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2024-11-16 15:25:26 -08:00
parent 3bd1f0c8a0
commit e5fb0a2929
3 changed files with 146 additions and 18 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
content/blog/03_spa_agda_fixed_height.md
View File

@@ -97,7 +97,8 @@ ordering relation `R`/`<` are expected to play together nicely (if `a < b`, and
{{< codelines "agda" "agda-spa/Chain.agda" 3 7 >}}
From there, the definition of the `Chain` data type is much like the definition
of a vector, but indexed by the endpoints, and containing witnesses of `R`/`<`
of [a vector from `Data.Vec`](https://agda.github.io/agda-stdlib/v2.0/Data.Vec.Base.html#1111),
but indexed by the endpoints, and containing witnesses of `R`/`<`
between its elements. The indexing allows for representing
the type of chains between particular lattice elements, and serves to ensure
concatenation and other operations don't merge disparate chains.