law set_out

minebender-game@1.0.0.0 · proof_lists.bend:92

import Base

92# Setting an index past the end changes nothing.
93law set_out:
94  for -A: Data
95  for +xs: List<&2, A>
96  for +i: Nat
97  for +v: A
98  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == False{} : Bool}
99  {List.set(&2, A, xs, i, v) == xs : List<&2, A>}