W64.red96: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as W64
Lines 395-399 of bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&start_line=395&end_line=399

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W

# (the zero test of hi(m) only guards the digit: red96 is called with
# hi(m) != 0; it also stops the proof checker from expanding the digit in
# every statement that names red96)
def red96(+xh: W.U64, +x0: U32, +m: W.U64) -> W.U64:
  red96_z(xh, x0, m, U32.is_zero(hi(m)))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=hi
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend&name=red96_z