law at_take

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

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

443law at_take:
444  for +n: Nat
445  for +xs: List<&2, U32>
446  for +i: Nat
447  for h: {Nat.is_lt(i, n) == True{} : Bool}
448  {B.at(B.take(n, xs), i) == B.at(xs, i) : Maybe<&2, U32>}