law get_set_self

bend-mathlib@0.8.1.0 · list.bend:1752

import Base

1752# Reading the index just set gives the new value wherever the index is in range.
1753law get_set_self:
1754  for -a: Quant
1755  for -A: Kind(a)
1756  for xs: List<a, A>
1757  for n: Nat
1758  for -x: A
1759  {List.get(a, A, List.set(a, A, xs, n, x), n) == Maybe.map(a, A, A, y => x, List.get(a, A, xs, n)) : Maybe<a, A>}