mbk/sized-array
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

right-pad

Browse source
This commit is contained in:
mehbark 2023-02-14 15:34:51 -05:00
parent 1ae5d8eb46
commit ed68082ee0
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
SizedArray.lean
View file

@ -528,3 +528,8 @@ def left_pad (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
exact left_pad' to with' xs hnle exact left_pad' to with' xs hnle
#eval left_pad 10 413 (from_list [1,2,3,4,5,6,7]) #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])