def sb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsrel.bend:18

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV

18# bits off + i - 1 down to off of K
19def sb(i: Nat, +off: Nat, +k: Nat) -> List<&2, Nat>:
20  match i:
21    case 0n: Nil{}
22    case 1n+ +j: CV.bit(Nat.add(off, j), k) <> sb(j, off, k)