address remaining TODO, fix issues with left-nesting for for and ext, add motivation blurb to the readme

1 files changed, 19 insertions, 0 deletions

diff --git a/examples/equality.makkai b/examples/equality.makkai
new file mode 100644
index 0000000..a9b3368
--- /dev/null
+++ b/examples/equality.makkai
@@ -0,0 +1,19 @@
+let set Empty = variant[]
+let set Unit = record {}
+let element pt : Unit = {}
+
+let set Three = variant [ zero : Unit | one : Unit | two : Unit ]
+
+let signature EqS = (x : Three) (y: Three) -> theory { E :: Set }
+let instance eqThree :: EqS = for (x: Three) (y: Three), {
+    .E = case x of [ zero. z => case y of [ zero. w => Unit :: Set | one. w => Empty :: Set | two. w => Empty :: Set ]
+                   | one. z => case y of [ zero. w => Empty :: Set | one. w => Unit :: Set | two. w => Empty :: Set ]
+                   | two. z => case y of [ zero. w => Empty :: Set | one. w => Empty :: Set | two. w => Unit :: Set ]
+                   ]
+}
+
+let set Diagonal = record { x : Three, y : Three, equal : set-of((eqThree x y) .E) }
+
+let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
+
+let element oopsOneEqualsTwo : Diagonal = { .x = one. pt, .y = two. pt, .equal = pt }