From ef3d7a3ce2d6686d37f1b2446d5de31b29f5cd00 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Mon, 27 Apr 2026 22:01:59 +0100
Subject: add tough example

---
 src/main.rs   | 8 ++++++++
 src/parser.rs | 9 +++++++++
 2 files changed, 17 insertions(+)

(limited to 'src')

diff --git a/src/main.rs b/src/main.rs
index ca9b9bb..3f6b3cc 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -31,6 +31,14 @@ let set Z_or_Float = variant [ z : Z | f : Float ]
 let element injected : Z_or_Float = z. z
 let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]
 
+// this should be difficult unless we correctly handle various forms of alpha/beta
+let signature OneSet = theory { F :: Set }
+let signature T = theory {
+    A :: Set,
+    B :: (x : set-of({ .F = A } .F)) -> Set,
+    C :: (x : set-of(A)) (b : set-of(B x)) -> Set
+}
+
 let signature Graph = theory {
     Node :: Set,
     Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
diff --git a/src/parser.rs b/src/parser.rs
index 0a7f063..65aa7f4 100644
--- a/src/parser.rs
+++ b/src/parser.rs
@@ -276,6 +276,15 @@ let set Maybe = variant [
     #[test]
     fn test_theories_and_instances() {
         let src = r#"
+            let signature OneSet = theory { F :: Set }
+
+            let signature T = theory {
+                A :: Set,
+                B :: (x : set-of({ .F = A } .F)) -> Set,
+                C :: (x : set-of(A)) (b : set-of(B x)) -> Set
+            }
+
+
             let signature Graph = theory {
                 Node :: Set,
                 Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
-- 
cgit v1.3.1