From c3b111ee9f0b1a5edef1ea2ede5c36a2b4c3ec26 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Wed, 1 Mar 2023 21:14:54 -0500
Subject: [PATCH] slicing a la rust

---
 NdArray.lean    |  0
 SizedArray.lean | 25 +++++++++++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 NdArray.lean

diff --git a/NdArray.lean b/NdArray.lean
new file mode 100644
index 0000000..e69de29
diff --git a/SizedArray.lean b/SizedArray.lean
index fa27c4c..ffbe768 100644
--- a/SizedArray.lean
+++ b/SizedArray.lean
@@ -533,3 +533,28 @@ def right_pad (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
   : SizedArray α (max to n) := xs |> reverse |> left_pad to with' |> reverse
 
 #eval right_pad 10 413 (from_list [1,2,3,4,5,6,7])
+
+notation xs "[" a " ... " b "]" => take (b - a) $ drop a xs
+notation xs "["   " ... " b "]" => take b xs
+notation xs "[" a " ..= " b "]" => take (b - (a - 1)) $ drop a xs
+notation xs "["   " ..= " b "]" => take (b + 1) xs
+-- ⦋⦌
+-- ⹗⹘
+def List.to_sized (xs : List α) := (from_list xs)
+
+#eval (from_list [1,2,3]) [1 ... 2]
+#eval (from_list [1,2,3]) [  ... 2]
+#eval (from_list [1,2,3]) [1 ..= 2]
+#eval (from_list [1,2,3]) [  ..= 2]
+
+def read_exact : α → α := id
+
+example : SizedArray UInt8 8 := Id.run do
+  let mut header := replicate (1 + 8 + 2) (0 : UInt8)
+  header := read_exact header
+  let bla := header [1 ... 9]
+  by
+    apply pure
+    have h : 8 = (min (9 - 1) (1 + 8 + 2 - 1)) := by simp
+    rw [← h] at bla
+    exact bla