Common.shift: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as Common
Lines 14-24 of bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&start_line=14&end_line=24

import Base

# Widths without powers: x * 2^k, n div 2^k and n mod 2^k by k doublings or
# halvings, and "n fits k bits". A literal 2^32 or 2^64 is beyond what the
# proof checker expands, so the fixed-width specifications (spec/math/generic,
# instances, w64) state widths through these; for a symbolic k they equal the
# pow2 forms (proofs/math/typed/width.bend).
def shift(k: Nat, +x: Nat) -> Nat:
  match k:
    case 0n:
      x
    case 1n+p:
      Nat.double(shift(p, x))

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double