def li.mask_take

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:145

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

145def li.mask_take(+n: Nat, +xs: List<&2, U32>) -> {B.mask(B.take(n, xs)) == B.take(n, B.mask(xs)) : List<&2, U32>}:
146  match n:
147    case 0n:
148      {==}
149    case 1n+p:
150      match xs:
151        case Nil{}:
152          {==}
153        case Con{+h, +t}:
154          %li.mask_take(p, t) : {Con{B.byte(h), B.mask(B.take(p, t))} == Con{B.byte(h), _} : List<&2, U32>}
155          {==}