prepare for more work on signatures, in particular this means processing records in telescoped contexts

rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type

1 files changed, 17 insertions, 17 deletions

diff --git a/src/main.rs b/src/main.rs
index 2b798e1..7d04891 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -19,35 +19,35 @@ fn main() {
 
     let src = r#"
 
-let set X = record { .b : Bool, .n : Nat } // basic
-
+// 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 }
-
-let set W = variant [ z. : Z | f. : Float ]
-
+// 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 element the_nat : Nat = z .y .n
-
-let element injected : W = z. z
-
-let element compute : Nat = case injected of [ z. myz => myz .y .n | f. myf => myf ]
+let signature Graph = theory {
+    .Node :: Set,
+    .Edge :: (s : Node) (t : Node) -> Set
+}
 
-// 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-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 programme = parser::parser::program(src);