1 files changed, 0 insertions, 47 deletions
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 84baa12..d769afe 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -777,53 +777,6 @@ data Block
     deriving (Show, Eq, Ord)
 
 
-data Task = Task
-    { taskDirectness :: Directness
-    , taskHypotheses :: [Hypothesis] -- ^ No guarantees on order.
-    , taskConjectureLabel :: Marker
-    , taskLocation :: Location
-    , taskConjecture :: Formula
-    } deriving (Show, Eq, Generic, Hashable)
-
-data Hypothesis = Hypothesis
-    { hypothesisMarker :: Marker
-    , hypothesisFormula :: Formula
-    }
-
-instance Show Hypothesis where
-    show (Hypothesis marker formula) =
-        "Hypothesis " <> show marker <> " " <> show formula
-
-instance Eq Hypothesis where
-    Hypothesis marker formula == Hypothesis marker' formula' =
-        (marker, formula) == (marker', formula')
-
-instance Ord Hypothesis where
-    compare (Hypothesis marker formula) (Hypothesis marker' formula') =
-        compare (marker, formula) (marker', formula')
-
-instance Hashable Hypothesis where
-    hashWithSalt salt (Hypothesis marker formula) =
-        hashWithSalt salt (marker, formula)
-
-
--- | Indicates whether a given proof is direct or indirect.
--- An indirect proof (i.e. a proof by contradiction) may
--- cause an ATP to emit a warning about contradictory axioms.
--- When we know that the proof is indirect, we want to ignore
--- this warning. For relevance filtering we also want to know
--- what our actual goal is, so we keep the original conjecture.
-data Directness
-    = Indirect Formula -- ^ The former conjecture.
-    | Direct
-    deriving (Show, Eq, Generic, Hashable)
-
-isIndirect :: Task -> Bool
-isIndirect task = case taskDirectness task of
-    Indirect _ -> True
-    Direct -> False
-
-
 -- | Full boolean contraction.
 contraction :: ExprOf a -> ExprOf a
 contraction = \case