From 065e0ddcc06d376bd34081366587d043f20b4312 Mon Sep 17 00:00:00 2001
From: tslil <tslil@posteo.de>
Date: Thu, 23 Apr 2026 14:54:24 +0100
Subject: Progress on checking sets

---
 src/main.rs | 34 +++++++++++++++++++---------------
 1 file changed, 19 insertions(+), 15 deletions(-)

(limited to 'src/main.rs')

diff --git a/src/main.rs b/src/main.rs
index 11357a9..a76dde4 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -16,21 +16,25 @@ fn main() {
 
     let src = r#"
 
-let set X = record { .b : Bool, .n : Nat }
-
-let element x : X = { .b = true, .n = 41, .x = 3.14 }
-
-let signature Graph = theory {
-    .Node :: Set,
-    .Edge :: (s : Node) (t : Node) -> Set
-}
-
-let instance natPoset :: Graph = {
-    .Node = Nat,
-    .Edge = for (s : Nat) (t : Nat), Bool
-}
-
-let element node : set(natPoset .Node) = 7
+let set X = record { .b : Bool, .n : Nat } // basic
+
+let set Y = X
+
+let set Z = record { .y : Y }
+
+// let element x : X = { .b = true, .n = 41, .x = 3.14 }
+//
+// let signature Graph = theory {
+//     .Node :: Set,
+//     .Edge :: (s : Node) (t : Node) -> Set
+// }
+//
+// let instance natPoset :: Graph = {
+//     .Node = Nat,
+//     .Edge = for (s : Nat) (t : Nat), Bool
+// }
+//
+// let element node : set(natPoset .Node) = 7
 "#;
     let programme = parser::parser::program(src);
 
-- 
cgit v1.3.1