diff --git a/Main.lean b/Main.lean
index fdeedcd..edbbfce 100644
--- a/Main.lean
+++ b/Main.lean
@@ -1,4 +1,4 @@
 import TenCert
 
 def main : IO Unit :=
-  IO.println s!"Hello, {hello}!"
+  IO.println s!"Hello, {TenCert.hello}!"
diff --git a/TenCert.lean b/TenCert.lean
index 4882595..7edd3ac 100644
--- a/TenCert.lean
+++ b/TenCert.lean
@@ -1,3 +1,6 @@
 -- This module serves as the root of the `TenCert` library.
 -- Import modules here that should be built as part of the library.
-import TenCert.Basic
\ No newline at end of file
+import TenCert.Basic
+import SHerLOC.Basic
+import ANPU.Basic
+import TensorLib.Basic
diff --git a/TenCert/Basic.lean b/TenCert/Basic.lean
index e99d3a6..f52a7be 100644
--- a/TenCert/Basic.lean
+++ b/TenCert/Basic.lean
@@ -1 +1,5 @@
-def hello := "world"
\ No newline at end of file
+namespace TenCert
+
+def hello := "world"
+
+namespace TenCert
diff --git a/lake-manifest.json b/lake-manifest.json
index 83f8a7e..e08f91b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,5 +1,35 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
- "packages": [],
+ "packages":
+ [{"url": "https://github.com/leanprover/SHerLOC.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "3e2777320ce9326f0f212acac583ffa864dafe89",
+   "name": "SHerLOC",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/ANPU.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "e989420b95f2c7c091bdb99459d87fdfdcd90898",
+   "name": "ANPU",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/TensorLib.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "8103ee2345c79143153213030ee2ebae7b809fe8",
+   "name": "TensorLib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
  "name": "TenCert",
  "lakeDir": ".lake"}
diff --git a/lakefile.lean b/lakefile.lean
index e720162..037123d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,6 +4,15 @@ open Lake DSL
 package "TenCert" where
   -- add package configuration options here
 
+require SHerLOC from git
+  "https://github.com/leanprover/SHerLOC.git" @ "main"
+
+require ANPU from git
+  "https://github.com/leanprover/ANPU.git" @ "main"
+
+require TensorLib from git
+  "https://github.com/leanprover/TensorLib.git" @ "main"
+
 lean_lib «TenCert» where
   -- add library configuration options here