Add Common.lean

`Common` is a module with a grabbag of functionality required by later files.
leanprover · Jan 3, 2025 · e365e9d · e365e9d
1 parent 142bb8e
commit e365e9d
Show file tree

Hide file tree

Showing 7 changed files with 586 additions and 69 deletions.
diff --git a/Main.lean b/Main.lean
@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jean-Baptiste Tristan, Paul Govereau, Sean McLaughlin
+-/
+
+import TensorLib
+
+def main (_args : List String) : IO UInt32 :=
+  return 0
diff --git a/TensorLib/Basic.lean b/TensorLib/Basic.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jean-Baptiste Tristan, Paul Govereau, Sean McLaughlin
+-/
+
+import TensorLib.Common