Npy file support

NumPy uses a custom binary format to store ndarrays. This file implements that format.
leanprover · Jan 3, 2025 · 1a19f81 · 1a19f81
1 parent 8be0e0d
commit 1a19f81
Show file tree

Hide file tree

Showing 3 changed files with 412 additions and 0 deletions.
diff --git a/TensorLib/Basic.lean b/TensorLib/Basic.lean
@@ -6,3 +6,4 @@ Authors: Jean-Baptiste Tristan, Paul Govereau, Sean McLaughlin
 
 import TensorLib.Common
 import TensorLib.Dtype
+import TensorLib.Npy
diff --git a/TensorLib/Common.lean b/TensorLib/Common.lean
@@ -137,6 +137,7 @@ Strides also are empty for scalar arrays.
 -/
 structure Shape where
   val : List Nat
+deriving Repr, Inhabited
 
 namespace Shape
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,3 +6,4 @@ Authors: Jean-Baptiste Tristan, Paul Govereau, Sean McLaughlin

		import TensorLib.Common
		import TensorLib.Dtype
		import TensorLib.Npy