def bits01

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsv.bend:54

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L

54def bits01(xs: List<&2, Nat>) -> {all01(L.bits(xs)) == True{} : Bool}:
55  match xs:
56    case Nil{}:
57      {==}
58    case +x <> +t:
59      all01_app(L.bits(t), L.bits_of(16n, x), bits01(t), bits_of01(16n, x))