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