def vg

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS

119# valo guarded on one: kept folded by the checker (see FS.gdigits)
120def vg(+one: Nat, xs: List<&2, U32>) -> Nat:
121  match one:
122    case 0n:
123      0n
124    case 1n+z:
125      valo(1n+z, xs)