law take_set_succ

lawful-bytes@0.1.1.0 · proof_seq.bend:82

import Base

82# Setting index n and keeping n + 1 elements: the first n, then v.
83law take_set_succ:
84  for +xs: List<&2, U32>
85  for +n: Nat
86  for +v: U32
87  for +h: {Nat.is_lt(n, List.length(&2, U32, xs)) == True{} : Bool}
88  {List.take(&2, U32, List.set(&2, U32, xs, n, v), Nat.add(n, 1n)) == List.append(&2, U32, List.take(&2, U32, xs, n), [v]) : List<&2, U32>}