def valo

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/consts.bend:23

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

23# the value of xs times one, digit by digit
24def valo(+one: Nat, xs: List<&2, U32>) -> Nat:
25  match xs:
26    case Nil{}:
27      0n
28    case Con{h, t}:
29      Nat.add(Nat.mul(one, U32.to_nat(h)), C.shift(8n, valo(one, t)))