def shn

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:33

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

33# 2^(8 n) x
34def shn(n: Nat, +x: Nat) -> Nat:
35  match n:
36    case 0n:
37      x
38    case 1n+m:
39      C.shift(8n, shn(m, x))