aboutsummaryrefslogtreecommitdiff
path: root/src/main.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/main.rs')
-rw-r--r--src/main.rs26
1 files changed, 18 insertions, 8 deletions
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);