From 617f3931de77bd795a97331e7146eb10266af7e9 Mon Sep 17 00:00:00 2001 From: tslil Date: Thu, 30 Apr 2026 10:52:07 +0100 Subject: lost track of what's going on --- src/main.rs | 26 ++++++++++++++++++-------- 1 file changed, 18 insertions(+), 8 deletions(-) (limited to 'src/main.rs') diff --git a/src/main.rs b/src/main.rs index 57e7f52..692379f 100644 --- a/src/main.rs +++ b/src/main.rs @@ -43,15 +43,15 @@ fn main() { // C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set // } -let signature Graph = theory { - Node :: Set, - Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set -} +// let signature Graph = theory { +// Node :: Set, +// Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set +// } -let instance natPoset :: Graph = { - .Node = Nat :: Set, - .Edge = for (s : Nat) (t : Nat), Bool :: Set -} +// let instance natPoset :: Graph = { +// .Node = Nat :: Set, +// .Edge = for (s : Nat) (t : Nat), Bool :: Set +// } // let element node : set-of(natPoset .Node) = 7 @@ -60,6 +60,16 @@ let instance natPoset :: Graph = { // target: set-of(natPoset .Node), // connected: set-of(natPoset .Edge source target) // } + +let signature S = theory { + A :: Set, + B :: (x : set-of(A)) -> Set +} + +let instance i :: S = { + .A = Nat :: Set, + .B = for (x : set-of(A)), Bool :: Set +} "#; let programme = parser::debug_parse(src); -- cgit v1.3.1