def pos

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

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

23# y at limb position n: y 2^(16 n)
24def pos(n: Nat, +y: Nat) -> Nat:
25  match n:
26    case 0n: y
27    case 1n+k: C.shift(16n, pos(k, y))