add tough example

2 files changed, 17 insertions, 0 deletions

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