diff --git a/SizedArray.lean b/SizedArray.lean index 2b7069d..fa27c4c 100644 --- a/SizedArray.lean +++ b/SizedArray.lean @@ -528,3 +528,8 @@ def left_pad (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n) exact left_pad' to with' xs hnle #eval left_pad 10 413 (from_list [1,2,3,4,5,6,7]) + +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])