def drop64

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/chacha8/stream.bend:21

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W

21def drop64(n: Nat, xs: List<&2, W.U64>) -> List<&2, W.U64>:
22  match n xs:
23    case 0n _:
24      xs
25    case 1n+p Nil{}:
26      []
27    case 1n+p Con{x, rest}:
28      drop64(p, rest)