W64.dig_t: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/math/w64.bend as W64
Lines 108-114 of bend-collections@1.0.0.0/src/math/w64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/math/w64.bend&start_line=108&end_line=114

import Base

# One digit of the long division by d: (r * base + g) / d and mod d, for a
# remainder r < d < 2^32 and a digit g < base = 2^16, so every partial
# dividend r * 2^16 + g is below 2^48 (the runtime's Nat bound). The low word
# is taken as two 16-bit digits; the base is written 256 * 256 so the proof
# checker never expands a 17-bit literal.
def dig_t(+r: Nat, +base: Nat, +g: Nat) -> Nat:
  Nat.add(Nat.mul(r, base), g)

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