From 8e4759bd2b24a5aa1e798053a968f5b80b5581d9 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 30 May 2024 20:52:33 -0700 Subject: [PATCH] Start on the navigation links in Agda SPA intro Signed-off-by: Danila Fedorin --- content/blog/00_spa_agda_intro.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/content/blog/00_spa_agda_intro.md b/content/blog/00_spa_agda_intro.md index 90802f7..8707c37 100644 --- a/content/blog/00_spa_agda_intro.md +++ b/content/blog/00_spa_agda_intro.md @@ -85,6 +85,9 @@ I'd like to cover the following major topics, spending a couple of posts on each CFGs that make sense, our analysis produces results that match the language's execution. -{{< todo >}} -Once the posts are ready, link them here to add some kind of navigation. -{{< /todo >}} + +### Navigation +Here are the posts that I’ve written so far for this series: + +* [Lattices]({{< relref "01_spa_agda_lattices" >}}) +* [Combining Lattices]({{< relref "02_spa_agda_combining_lattices" >}})