namespace

leanprover · Sep 20, 2024 · 3dd0975 · 3dd0975
1 parent 8015209
commit 3dd0975
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/TensorLib/Basic.lean b/TensorLib/Basic.lean
@@ -1 +1,5 @@
-def hello := "world"
+namespace TensorLib
+
+def hello := "world"
+
+end TensorLib