Slicing

Implements Python's slice operator, commonly used in NumPy indexing.
leanprover · Jan 2, 2025 · 6b6c404 · 6b6c404
1 parent f82c5cb
commit 6b6c404
Show file tree

Hide file tree

Showing 2 changed files with 418 additions and 0 deletions.
diff --git a/TensorLib/Basic.lean b/TensorLib/Basic.lean
@@ -8,3 +8,4 @@ import TensorLib.Common
 import TensorLib.Dtype
 import TensorLib.Npy
 import TensorLib.Broadcast
+import TensorLib.Slice