law list_mask_take

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:52

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

52law list_mask_take:
53  for +n: Nat
54  for +xs: List<&2, U32>
55  {B.mask(B.take(n, xs)) == B.take(n, B.mask(xs)) : List<&2, U32>}