Start on indexed data

AleAndForCode · Aug 14, 2024 · 8f42d48 · 8f42d48
1 parent a6e7132
commit 8f42d48
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 0 deletions.
diff --git a/build.sbt b/build.sbt
@@ -131,6 +131,7 @@ lazy val pages = List(
   "indexed-types/index.md",
   "indexed-types/phantom-type.md",
   "indexed-types/codata.md",
+  "indexed-types/data.md",
   "indexed-types/conclusions.md",
   // Interpreter optimization
   "adt-optimization/index.md",

diff --git a/src/pages/indexed-types/data.md b/src/pages/indexed-types/data.md
@@ -0,0 +1,3 @@
+## Indexed Data
+
+The key idea of indexed data is to encode type equalities in data.