def hv_app

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

import Base

25def hv_app(+one: Nat, xs: List<&2, Nat>, +e: Nat, +ys: List<&2, Nat>) -> {hv(List.append(&2, Nat, xs, ys), one, e) == hv(ys, one, hv(xs, one, e)) : Nat}:
26  match xs:
27    case Nil{}:
28      {==}
29    case +x <> +t:
30      hv_app(one, t, Nat.add(Nat.mul(x, one), Nat.double(e)), ys)