Add Tensor type

Multi-dimensional arrays
leanprover · Jan 4, 2025 · 5a52db1 · 5a52db1
1 parent 1a5aa13
commit 5a52db1
Show file tree

Hide file tree

Showing 3 changed files with 496 additions and 0 deletions.
diff --git a/TensorLib/Basic.lean b/TensorLib/Basic.lean
@@ -9,3 +9,4 @@ import TensorLib.Dtype
 import TensorLib.Npy
 import TensorLib.Broadcast
 import TensorLib.Slice
+import TensorLib.Tensor
diff --git a/TensorLib/Common.lean b/TensorLib/Common.lean
@@ -142,13 +142,17 @@ deriving BEq, Repr, Inhabited
 
 namespace Shape
 
+def empty : Shape := Shape.mk []
+
 --! The number of elements in a tensor. All that's needed is the shape for this calculation.
 -- TODO: Put this in the struct?
 def count (shape : Shape) : Nat := natProd shape.val
 
 --! Number of dimensions
 def ndim (shape : Shape) : Nat := shape.val.length
 
+def map (shape : Shape) (f : List Nat -> List Nat) : Shape := Shape.mk (f shape.val)
+
 /-!
 Strides can be computed from the shape by figuring out how many elements you
 need to jump over to get to the next spot and mulitplying by the bytes in each