From 77d637846be1eb0d140612731c80ca7a6cf1bb29 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Thu, 7 May 2026 15:33:30 +0100
Subject: fix failure to add hypotheticals for instances of compound signatures

---
 examples/equality.makkai              |  2 +-
 examples/tests/test_projection.makkai | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 examples/tests/test_projection.makkai

(limited to 'examples')

diff --git a/examples/equality.makkai b/examples/equality.makkai
index 86b81ae..294dafc 100644
--- a/examples/equality.makkai
+++ b/examples/equality.makkai
@@ -54,7 +54,7 @@ let signature NeqParticular = theory {
     Neq :: (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))) -> <Empty>
 }
 
-let instance zeroNeqOne :: NeqParticular = {
+let instance zeroNeqOneAgain :: NeqParticular = {
     .SE = eqTwo,
     .A = <zero. pt>,
     .B = <one. pt>,
diff --git a/examples/tests/test_projection.makkai b/examples/tests/test_projection.makkai
new file mode 100644
index 0000000..2c4ce23
--- /dev/null
+++ b/examples/tests/test_projection.makkai
@@ -0,0 +1,10 @@
+let signature S = theory {
+    A :: Set,
+    Point :: <A>,
+    B :: (x : set-of(A)) -> Set
+}
+
+let signature T = theory {
+    SI :: S,
+    F :: (r: set-of((SI .B) (element-of(SI .Point)))) -> Set
+}
-- 
cgit v1.3.1