From 8fc5a0fbda9742b7b906893e9acc62c15bdcca3b Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Sat, 15 Mar 2025 18:22:52 -0400
Subject: [PATCH] FreshLists skeleton

---
 db/posts/7.json                                  | 16 ++++++++++++++++
 db/series/1.json                                 |  7 +++++++
 projects/Idris/Idris.ipkg                        |  1 +
 .../Idris/src/DependentNuggets/FreshLists.md     |  8 ++++++++
 4 files changed, 32 insertions(+)
 create mode 100644 db/posts/7.json
 create mode 100644 db/series/1.json
 create mode 100644 projects/Idris/src/DependentNuggets/FreshLists.md

diff --git a/db/posts/7.json b/db/posts/7.json
new file mode 100644
index 0000000..a2a5700
--- /dev/null
+++ b/db/posts/7.json
@@ -0,0 +1,16 @@
+{
+  "edited-at": [
+  ],
+  "hidden": false,
+  "idris": true,
+  "ipkg": "/home/nathan/Projects/Blog/projects/Idris/Idris.ipkg",
+  "posted-at": "2025-03-15T18:07:00.649227-04:00",
+  "slugs": [
+  ],
+  "source": "/home/nathan/Projects/Blog/projects/Idris/src/DependentNuggets/FreshLists.md",
+  "source-code": "https://git.stranger.systems/thatonelutenist/website/src/branch/trunk/projects/Idris/src/DependentNuggets/FreshLists.md",
+  "special": false,
+  "tags": [
+    "idris"
+  ]
+}
\ No newline at end of file
diff --git a/db/series/1.json b/db/series/1.json
new file mode 100644
index 0000000..94f387d
--- /dev/null
+++ b/db/series/1.json
@@ -0,0 +1,7 @@
+{
+  "desc": "Introductions to the building blocks of dependently typed programs.",
+  "post-ids": [
+    7
+  ],
+  "title": "Dependent Nuggets"
+}
\ No newline at end of file
diff --git a/projects/Idris/Idris.ipkg b/projects/Idris/Idris.ipkg
index 8331301..ce522e4 100644
--- a/projects/Idris/Idris.ipkg
+++ b/projects/Idris/Idris.ipkg
@@ -19,6 +19,7 @@ authors = "Nathan McCarty"
 modules = Idris
         , Posts.HelloWorld
         , LessMacrosMoreTypes.Printf
+        , DependentNuggets.FreshLists
 
 -- main file (i.e. file to load at REPL)
 -- main =
diff --git a/projects/Idris/src/DependentNuggets/FreshLists.md b/projects/Idris/src/DependentNuggets/FreshLists.md
new file mode 100644
index 0000000..2998e8b
--- /dev/null
+++ b/projects/Idris/src/DependentNuggets/FreshLists.md
@@ -0,0 +1,8 @@
+# FreshLists: Containers That Only Accept "Fresh" Elements
+
+```idris hide
+module DependentNuggets.FreshLists
+```
+
+When programming, we quite frequently encounter the for a data structure that can contain at most one of each given element. Typically, we would use a `Set`, which satisfies this constraint, but does so as a runtime invariant that must be taken on trust, and results in ergonomic concerns when used as a component of API design.
+