diff --git a/src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean b/src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean
new file mode 100644
index 0000000000..8fe6126788
--- /dev/null
+++ b/src/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.LinearArith.Solver
+import Lean.Meta.Tactic.LinearArith.Nat.Basic
+
+namespace Lean.Meta.Linear.Nat
+
+namespace Collect
+
+structure Cnstr where
+  cnstr : LinearArith
+  proof : Expr
+
+structure State where
+  cnstrs : Array Cnstr
+
+abbrev M := StateRefT State ToLinear.M
+
+-- TODO
+
+end Collect
+
+end Lean.Meta.Linear.Nat