English
Update s at position n by applying f to the nth element, if it exists; otherwise leave unchanged.
Русский
Обновить последовательность s на позиции n путем применения f к i-й (i = n) элементу, если он существует; иначе оставить без изменений.
LaTeX
$$$ \mathrm{update}(s,n,f) : \mathrm{Seq}(\alpha) \to \mathrm{Seq}(\alpha),\quad \mathrm{update}(s,n,f).\mathrm{val} = \mathrm{Function.update}(s.\mathrm{val}, n, (s.\mathrm{val}\ n).map(f)).$$$
Lean4
/-- Applies `f` to the `n`th element of the sequence, if it exists, replacing that element
with the result. -/
def update (s : Seq α) (n : ℕ) (f : α → α) : Seq α
where
val := Function.update s.val n ((s.val n).map f)
property :=
by
have (i : ℕ) : Function.update s.val n ((s.get? n).map f) i = none ↔ s.get? i = none := by
by_cases hi : i = n <;> simp [Function.update, hi]
simp only [IsSeq, val_eq_get, this]
exact @s.prop
