[ clause ] Move ProblemEq. Maybe it's time to release a newer version?

src/check/rules/clause.rs

@@ -1,7 +1,18 @@
 use crate::check::monad::{TCM, TCS};
-use crate::syntax::abs::{AbsClause, AbsCopat, ProblemEq};
+use crate::syntax::abs::{AbsClause, AbsCopat};
 use crate::syntax::core::{Clause, Pat, Tele, Term, Val};
 
+/// A user pattern and a core term that they should equal
+/// after splitting is complete.
+/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#ProblemEq).
+#[derive(Debug, PartialEq, Eq, Clone)]
+pub struct ProblemEq {
+    /// The pattern causes this problem.
+    in_pat: AbsCopat,
+    inst: Term,
+    ty: Term,
+}
+
 /// User patterns we still have to split on.
 /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.TypeChecking.Rules.LHS.Problem.html#Problem).
 #[derive(Debug, Clone)]

src/syntax/abs/decl.rs

@@ -2,8 +2,6 @@ use voile_util::level::Level;
 use voile_util::loc::{Ident, Loc, ToLoc};
 use voile_util::uid::GI;
 
-use crate::syntax::core::Term;
-
 use super::{Abs, AbsCopat, AbsTele};
 
 /// Declaration.
@@ -131,16 +129,6 @@ impl ToLoc for AbsDecl {
     }
 }
 
-/// A user pattern and a core term that they should equal
-/// after splitting is complete.
-/// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#ProblemEq).
-#[derive(Debug, PartialEq, Eq, Clone)]
-pub struct ProblemEq {
-    in_pat: AbsCopat,
-    inst: Term,
-    ty: Term,
-}
-
 /// Clause information in abstract syntax.
 /// [Agda](https://hackage.haskell.org/package/Agda-2.6.0.1/docs/src/Agda.Syntax.Abstract.html#Clause%27).
 #[derive(Debug, PartialEq, Eq, Clone)]