def take_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/lists.bend:42

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

42def take_zero(-A: Data, +ys: List<&2,A>) -> {SC.take(A,ys,0n) == Nil{} : List<&2,A>}:
43  match ys:
44    case Nil{}: {==}
45    case Con{+b,+u}: {==}