advancing

eneoli · Dec 7, 2024 · c411b7a · c411b7a
1 parent 58eb4c3
commit c411b7a
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/src/kernel/checker/synthesize.rs b/src/kernel/checker/synthesize.rs
@@ -263,6 +263,7 @@ impl<'a> ProofTermVisitor<Result<(Type, TypeCheckerResult), SynthesizeError>>
 
         match (&bound_param_type, &body_type) {
             // Forall
+            // TODO name clash
             (Type::Datatype(datatype_ident), Type::Prop(body_type)) => {
                 let _type = body_type.bind_identifier(
                     QuantifierKind::ForAll,

diff --git a/src/main.rs b/src/main.rs
@@ -14,7 +14,7 @@ fn main() {
     // Step 1: Parse tokens
     let tokens = lexer().parse(src.clone());
 
-    println!("{:#?}", tokens);
+    // println!("{:#?}", tokens);
 
     if let Err(err) = tokens.clone() {
         err.into_iter().for_each(|e| {
@@ -48,7 +48,7 @@ fn main() {
         return;
     }
 
-    let fol = "A -> A";
+    let fol = "A";
     let fol_tokens = lexer().parse(fol).unwrap();
     let fol_len = fol.chars().count();
 
@@ -66,7 +66,7 @@ fn main() {
 
     // Step 3: Preprocess ProofTerm
 
-    println!("{:#?}", processed_proof);
+    // println!("{:#?}", processed_proof);
 
     // println!("{:#?}", prop.get_free_parameters());
 
@@ -78,11 +78,11 @@ fn main() {
 
     println!("{:#?}", _type);
 
-    println!("{}", prove(&prop).unwrap());
+    // println!("{}", prove(&prop).unwrap());
 
-    let ocaml_exporter = OcamlExporter::new();
+    // let ocaml_exporter = OcamlExporter::new();
 
-    println!("{}", ocaml_exporter.export(&processed_proof.proof_term));
+    // println!("{}", ocaml_exporter.export(&processed_proof.proof_term));
 
     // let proof_tree = ProofTree {
     //     premisses: vec![