slicing a la rust

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