def drop_zero

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

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

37def drop_zero(-A: Data, +ys: List<&2,A>) -> {SC.drop(A,ys,0n) == ys : List<&2,A>}:
38  match ys:
39    case Nil{}: {==}
40    case Con{+b,+u}: {==}