This commit is contained in:
mehbark 2023-02-13 21:09:32 -05:00
parent 038067e122
commit a5040e9b84

View file

@ -492,3 +492,36 @@ def take {from_len : Nat} (n : Nat) (xs : SizedArray α from_len)
-- example : SizedArray Nat 3 := take 3 (by simp) (from_list [1,2,3,4,5]) -- example : SizedArray Nat 3 := take 3 (by simp) (from_list [1,2,3,4,5])
#eval from_list [1,2,3,4,5,6,7,8,9,10] |> take 7 |> drop 2 |> reverse |> map (· * 2) |> (tail (by simp) ·) #eval from_list [1,2,3,4,5,6,7,8,9,10] |> take 7 |> drop 2 |> reverse |> map (· * 2) |> (tail (by simp) ·)
def left_pad' (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
(h : n ≤ to)
: SizedArray α to := by
let pad_amt := to - n
let (h₂ : pad_amt = to - n) := rfl
let padding := replicate pad_amt with'
let padded := append padding xs
rw [h₂] at padded
rw [Nat.sub_add_cancel] at padded
exact padded
exact h
def left_pad (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
: SizedArray α (max to n) := by
cases hle : (decide (to ≤ n)) with
| true =>
rw [max, Nat.instMaxNat, maxOfLe]
simp
let hle : to ≤ n := of_decide_eq_true hle
simp [hle]
exact xs
| false =>
let hle : ¬to ≤ n := of_decide_eq_false hle
let hnle := hle
rw [Nat.not_le_eq, ← Nat.succ_eq_add_one] at hnle
let hnle := Nat.le_of_succ_le hnle
rw [max, Nat.instMaxNat, maxOfLe]
simp
simp [hle]
exact left_pad' to with' xs hnle