def take_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/okm.bend:18

import Base

18def take_zero(+xs: List<&2, U32>) -> {List.take(&2, U32, xs, 0n) == Nil{} : List<&2, U32>}:
19  match xs:
20    case Nil{}:
21      {==}
22    case x <> rest:
23      {==}