From ed68082ee0498e16994217145582c19d32c9816c Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 14 Feb 2023 15:34:51 -0500
Subject: [PATCH] right-pad

---
 SizedArray.lean | 5 +++++
 1 file changed, 5 insertions(+)

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])