def hd_tl_v

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/limbs.bend:159

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

159def hd_tl_v(xs: List<&2, Nat>) -> {ev(xs) == Nat.add(L.hd0(xs), C.shift(16n, ev(L.tl(xs)))) : Nat}:
160  match xs:
161    case Nil{}:
162      {==}
163    case x <> t:
164      {==}