English
shiftRightFill(v,i,fill) shifts v to the right by i positions and fills the beginning with fill; if length is insufficient, replicate fill.
Русский
shiftRightFill(v,i,fill) сдвигает v вправо на i позиций и заполняет начало значением fill; при недостаточной длине заполняемость повторяется.
LaTeX
$$$\\text{shiftRightFill}(v,i,fill) = \\text{Vector.congr}(\\text{omega proof})\\big(\\text{replicate}(\\min n\\; i)\\; fill \\;\\;\\; ++\\; \\text{take}(n-i)\\; v\\big)$$$
Lean4
/-- `shiftRightFill v i` is the vector obtained by right-shifting `v` `i` times and padding with the
`fill` argument. If `v.length < i` then this will return `replicate n fill`. -/
def shiftRightFill (v : Vector α n) (i : ℕ) (fill : α) : Vector α n :=
Vector.congr (by omega) (replicate (min n i) fill ++ take (n - i) v)
