delete is-implemented and older style code

comment out a lot of tests

Author: nikomatsakis

crates/formality-check/src/lib.rs

@@ -1,3 +1,5 @@
+#![allow(dead_code)]
+
 use std::collections::VecDeque;
 
 use anyhow::bail;
@@ -28,9 +30,8 @@ pub fn check_all_crates(program: &Program) -> Fallible<()> {
 }
 
 /// Checks the current crate in the program, assuming all other crates are valid.
-fn check_current_crate(program: &Program) -> Fallible<()> {
-    let db = Db::new(program.clone());
-    Check { program, db }.check()
+fn check_current_crate(_program: &Program) -> Fallible<()> {
+    todo!()
 }
 
 mod adts;

crates/formality-check/src/where_clauses.rs

@@ -63,8 +63,7 @@ impl super::Check<'_> {
                 self.prove_goal(env, assumptions, a.well_formed())?;
                 self.prove_goal(env, assumptions, b.well_formed())?;
             }
-            APR::AtomicPredicate(AtomicPredicate::HasImpl(_))
-            | APR::AtomicRelation(AtomicRelation::Equals(_, _))
+            APR::AtomicRelation(AtomicRelation::Equals(_, _))
             | APR::AtomicRelation(AtomicRelation::Sub(_, _)) => {
                 panic!("predicate would never appear directly in program text")
             }

crates/formality-decl/src/db.rs

@@ -24,10 +24,6 @@ impl formality_logic::Database for Program {
                     trait_id: _,
                     parameters,
                 })
-                | AtomicPredicate::HasImpl(TraitRef {
-                    trait_id: _,
-                    parameters,
-                })
                 | AtomicPredicate::NormalizesTo(
                     AliasTy {
                         name: _,

crates/formality-decl/src/lib.rs

@@ -2,8 +2,5 @@
 
 use formality_types::derive_links;
 
-pub mod db;
 pub mod grammar;
 pub mod orphan_rules;
-pub mod test;
-pub mod to_clause;