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

5 files changed, 40 insertions, 0 deletions

diff --git a/examples/alpha_equiv.makkai b/examples/alpha_equiv.makkai
new file mode 100644
index 0000000..2ae067a
--- /dev/null
+++ b/examples/alpha_equiv.makkai
@@ -0,0 +1,4 @@
+let signature S = (n : Nat) -> Set
+let signature T = (m : Nat) -> Set
+let instance i :: S = for (x : Nat), (Nat :: Set)
+let instance j :: T = i
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 }
diff --git a/examples/ext_codomain.makkai b/examples/ext_codomain.makkai
new file mode 100644
index 0000000..da0ddae
--- /dev/null
+++ b/examples/ext_codomain.makkai
@@ -0,0 +1,5 @@
+let signature S = (x : Nat) -> theory { G :: Set }
+
+let instance s :: S = for (x : Nat), { .G = (Nat :: Set) }
+
+let set NatAgain = set-of((s 42) .G)
diff --git a/examples/inline_nested.makkai b/examples/inline_nested.makkai
new file mode 100644
index 0000000..e891349
--- /dev/null
+++ b/examples/inline_nested.makkai
@@ -0,0 +1,9 @@
+let signature Outer = theory {
+    Inner :: theory { F :: Set }
+}
+
+let instance my_outer :: Outer = {
+    .Inner = { .F = (Nat :: Set) }
+}
+
+let set MyF = set-of(my_outer .Inner .F)
diff --git a/examples/nested_for.makkai b/examples/nested_for.makkai
new file mode 100644
index 0000000..b3618cc
--- /dev/null
+++ b/examples/nested_for.makkai
@@ -0,0 +1,3 @@
+let signature F = (n : Nat) -> (m : Nat) -> Set
+let instance f :: F = for (n : Nat), for (m : Nat), (Nat :: Set)
+let set Result = set-of(f 1 2)