Hash.x64.bytes: def of bend-kit-hash@0.3.0.2
Import: import bend-kit-hash@0.3.0.2/hash.bend as Hash
Lines 562-572 of bend-kit-hash@0.3.0.2/hash.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-hash@0.3.0.2/hash.bend&start_line=562&end_line=572

import Base

# The last len % 8 bytes: a 4-byte lane when there is one, then single bytes.
def x64.bytes(four: Bool, +k: Nat, h: W64, m: W64) -> W64:
  match four:
    case True{}:
      match m:
        case W64{+hi, +lo}:
          tail(~W64, ~x64.byte, k, hi, x64.four(h, lo))
    case False{}:
      match m:
        case W64{hi, +lo}:
          tail(~W64, ~x64.byte, k, lo, h)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-kit-hash@0.3.0.2/hash.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-kit-hash@0.3.0.2/hash.bend&name=tail
  https://jend.leeeet.dev/definition.txt?path=bend-kit-hash@0.3.0.2/hash.bend&name=x64.byte
  https://jend.leeeet.dev/definition.txt?path=bend-kit-hash@0.3.0.2/hash.bend&name=x64.four