391def magnitudeDivideStep =
392 (lambda unrestricted divisor : Bytes .
393 (lambda unrestricted digit : Byte .
394 (lambda unrestricted state : (sigma unrestricted quotient : BytesBuilder . Bytes) .
395 (app
396 (lambda unrestricted next : (sigma unrestricted quotientDigit : Nat . Bytes) .
397 (pair
398 (sigma unrestricted quotient : BytesBuilder . Bytes)
399 (bytes-builder-append
400 (bytes-builder-chunk (bytes-cons (nat-to-byte (first next)) b""))
401 (first state))
402 (second next)))
403 (magnitudeDivideDigit divisor (magnitudeNormalize (bytes-cons digit (second state))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.