aboutsummaryrefslogtreecommitdiff
path: root/src/main.rs
diff options
context:
space:
mode:
Diffstat (limited to 'src/main.rs')
-rw-r--r--src/main.rs10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/main.rs b/src/main.rs
index 94a9428..f721ef4 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -31,6 +31,10 @@ fn main() {
// 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 {
@@ -57,11 +61,7 @@ let set NatEdges = record {
connected: set-of(natPoset .Edge source target)
}
"#;
- let programme = parser::parser::program(src);
-
- assert!(programme.is_ok());
- let programme = programme.unwrap();
- println!("Parsed:\n```\n{}\n```\n", programme);
+ let programme = parser::debug_parse(src);
if let Err(e) = programme.check() {
println!("{}", e);