Internal canonical comparison can decide unequal digit lengths immediately.
This avoids repeatedly scanning a long divisor for shorter partial remainders.
202def magnitudeCompareCanonical =
203 (lambda unrestricted left : Bytes .
204 (lambda unrestricted right : Bytes .
205 (app
206 (nat-eliminate
207 (lambda unrestricted shorter : Nat . (pi unrestricted force : Nat . Nat))
208 (lambda unrestricted force : Nat .
209 (app
210 (nat-eliminate
211 (lambda unrestricted longer : Nat . (pi unrestricted force : Nat . Nat))
212 (lambda unrestricted force : Nat . (magnitudeCompareSameLength left right))
213 (lambda unrestricted predecessor : Nat .
214 (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
215 (lambda unrestricted force : Nat . (succ (succ zero)))))
216 (nat-less-than (bytes-length right) (bytes-length left)))
217 zero))
218 (lambda unrestricted predecessor : Nat .
219 (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
220 (lambda unrestricted force : Nat . (succ zero))))
221 (nat-less-than (bytes-length left) (bytes-length right)))
222 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.