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

1 files changed, 9 insertions, 0 deletions

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)