fill in some more todos

1 files changed, 11 insertions, 48 deletions

diff --git a/src/main.rs b/src/main.rs
index 692379f..34d6360 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -18,57 +18,20 @@ fn main() {
         .init();
 
     let src = r#"
+let signature Graph = theory {
+    Node :: Set,
+    Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
+}
 
-// let X be the set Y, call it Z
-// let set X = record { b : Bool, n : Nat }
-// let set Y = X
-// let set Z = record { y : Y }
-// make some elements
-// let element x : X = { .b = true, .n = 41 }
-// let element z : Z = { .y = x }
-// exercise case matching
-// 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 ]
-
-// 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 element e : set-of(natPoset .Edge 3 5) = true
-
-// 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(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 instance natPoset :: Graph = {
-//     .Node = Nat :: Set,
-//     .Edge = for (s : Nat) (t : Nat), Bool :: Set
-// }
-
-// let element node : set-of(natPoset .Node) = 7
-
-// let set NatEdges = record {
-//   source: set-of(natPoset .Node),
-//   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 natGraph :: Graph = {
+    .Node = Nat :: Set,
+    .Edge = for (s : Nat) (t : Nat), Bool :: Set
 }
 
-let instance i :: S = {
-  .A = Nat :: Set,
-  .B = for (x : set-of(A)), Bool :: Set
+let set NatEdges = record {
+  source: set-of(natGraph .Node),
+  target: set-of(natGraph .Node),
+  connected: set-of(natGraph .Edge source target)
 }
 "#;
     let programme = parser::debug_parse(src);