345def magnitudeSubtract =
346 (lambda unrestricted left : Bytes .
347 (lambda unrestricted right : Bytes .
348 (app
349 (nat-eliminate
350 (lambda unrestricted underflow : Nat . (pi unrestricted force : Nat . Bytes))
351 (lambda unrestricted force : Nat . (magnitudeSubtractOrdered left right))
352 (lambda unrestricted predecessor : Nat .
353 (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
354 (lambda unrestricted force : Nat . b"")))
355 (magnitudeLess left right))
356 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.