law take_drop

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

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

38law take_drop:
39  for n: Nat
40  for xs: List<&2, U32>
41  {B.append(B.take(n, xs), B.drop(n, xs)) == xs : List<&2, U32>}

Uses (6)

Used by (4)