Start on indexed data

noelwelsh · noelwelsh · commit 8f42d48712ca · 2024-08-14T12:34:58.000+01:00
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.

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+## Indexed Data`
	`2`	`+`
	`3`	`+The key idea of indexed data is to encode type equalities in data.`