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 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src/main.rs')

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
-- 
cgit v1.3.1