law at_append_lt

bend-osdev-bytes@0.1.1.0 · LAWS.bend:430

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

430law at_append_lt:
431  for +a: List<&2, U32>
432  for +b: List<&2, U32>
433  for +i: Nat
434  for h: {Nat.is_lt(i, B.len(a)) == True{} : Bool}
435  {B.at(B.append(a, b), i) == B.at(a, i) : Maybe<&2, U32>}