def sc_take_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:323

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

323def sc_take_zero(-A: Data, +xs: List<&2, A>) -> {SC.take(A, xs, 0n) == Nil{} : List<&2, A>}:
324  match xs:
325    case Nil{}:
326      {==}
327    case Con{a, t}:
328      {==}