313def magnitudeSubtractOrdered =
314 (lambda unrestricted left : Bytes .
315 (lambda unrestricted right : Bytes .
316 (magnitudeNormalize
317 (bytes-builder-build
318 (app
319 (bytes-eliminate
320 (lambda unrestricted rest : Bytes .
321 (pi unrestricted right : Bytes . (pi unrestricted borrow : Nat . BytesBuilder)))
322 (lambda unrestricted right : Bytes .
323 (lambda unrestricted borrow : Nat . (bytes-builder-empty)))
324 (lambda unrestricted head : Byte .
325 (lambda unrestricted tail : Bytes .
326 (lambda unrestricted continue : (pi unrestricted right : Bytes . (pi unrestricted borrow : Nat . BytesBuilder)) .
327 (lambda unrestricted right : Bytes .
328 (lambda unrestricted borrow : Nat .
329 (app
330 (lambda unrestricted subtrahend : Nat .
331 (app
332 (lambda unrestricted nextBorrow : Nat .
333 (bytes-builder-append
334 (bytes-builder-chunk
335 (bytes-cons
336 (magnitudeSubtractDigit head subtrahend nextBorrow)
337 b""))
338 (continue (bytes-tail right) nextBorrow)))
339 (magnitudeSubtractBorrow head subtrahend)))
340 (Std.Natural/naturalAdd (byte-to-nat (bytes-head right)) borrow)))))))
341 left)
342 right
343 zero)))))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.