Bits.parts: def of bend-kit-bits@0.1.0.1
Import: import bend-kit-bits@0.1.0.1/bits.bend as Bits
Lines 138-146 of bend-kit-bits@0.1.0.1/bits.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-bits@0.1.0.1/bits.bend&start_line=138&end_line=146

import Base
import bend-kit-bytes@0.3.3.0/bytes.bend as Bytes

# The parts of an n-bit v that land in word k and word k + 1, as stored words.
def parts(msb: Bool, +s: U32, +n: U32, +v: U32) -> U32 & U32:
  match msb:
    case True{}:
      +t = U32.shln(v, U32.to_nat((32 - n : U32)))
      (Bytes.bswap(U32.shrn(t, U32.to_nat(s))), Bytes.bswap(U32.shln(t, U32.to_nat((32 - s : U32)))))
    case False{}:
      +m = (v .&. mask(n) : U32)
      (U32.shln(m, U32.to_nat(s)), U32.shrn(m, U32.to_nat((32 - s : U32))))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-kit-bits@0.1.0.1/bits.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=bend-kit-bytes@0.3.3.0/bytes.bend&name=bswap