1module Compiler.NaturalMagnitudeArithmetic
2
3import Std.Natural
4
5-- Internal arithmetic on canonical decimal digit bytes, least significant first.
6-- Zero is empty; every digit is 0..9 and the final digit is nonzero.
7-- The checked owner validates external input before calling these operations.
8-- Whole-value Nat conversion is only for existing unary values or bounded carries.
9-- Normalization and addition assemble a BytesBuilder and materialize once;
10-- repeated bytes-cons of complete suffixes would copy quadratic byte volume.
11-- A carry digit uses explicit low-byte conversion of total + 246 for total
12-- in 10..19, which equals total - 10. Addition preserves canonical inputs.
13def magnitudeNormalize =
14 (lambda unrestricted digits : Bytes .
15 (bytes-builder-build
16 (second
17 (bytes-eliminate
18 (lambda unrestricted rest : Bytes . (sigma unrestricted active : Nat . BytesBuilder))
19 (pair (sigma unrestricted active : Nat . BytesBuilder) zero (bytes-builder-empty))
20 (lambda unrestricted head : Byte .
21 (lambda unrestricted tail : Bytes .
22 (lambda unrestricted continue : (sigma unrestricted active : Nat . BytesBuilder) .
23 (app
24 (nat-eliminate
25 (lambda unrestricted flag : Nat .
26 (pi unrestricted force : Nat .
27 (sigma unrestricted active : Nat . BytesBuilder)))
28 (lambda unrestricted force : Nat .
29 (pair
30 (sigma unrestricted active : Nat . BytesBuilder)
31 (succ zero)
32 (bytes-builder-append
33 (bytes-builder-chunk (bytes-cons head b""))
34 (second continue))))
35 (lambda unrestricted predecessor : Nat .
36 (lambda unrestricted induction : (pi unrestricted force : Nat . (sigma unrestricted active : Nat . BytesBuilder)) .
37 (lambda unrestricted force : Nat . continue)))
38 (Std.Natural/naturalAnd
39 (byte-equal head (byte 0))
40 (Std.Natural/naturalIsZero (first continue))))
41 zero))))
42 digits))))
43
44def magnitudeEqual =
45 (lambda unrestricted left : Bytes .
46 (lambda unrestricted right : Bytes .
47 (bytes-equal (magnitudeNormalize left) (magnitudeNormalize right))))
48
49def magnitudeSuccessorDigits =
50 (lambda unrestricted digits : Bytes .
51 (app
52 (bytes-eliminate
53 (lambda unrestricted rest : Bytes . (pi unrestricted force : Nat . Bytes))
54 (lambda unrestricted force : Nat . (bytes 1))
55 (lambda unrestricted head : Byte .
56 (lambda unrestricted tail : Bytes .
57 (lambda unrestricted continue : (pi unrestricted force : Nat . Bytes) .
58 (lambda unrestricted force : Nat .
59 (app
60 (nat-eliminate
61 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
62 (lambda unrestricted force : Nat .
63 (bytes-cons (nat-to-byte (succ (byte-to-nat head))) tail))
64 (lambda unrestricted predecessor : Nat .
65 (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
66 (lambda unrestricted force : Nat . (bytes-cons (byte 0) (continue zero)))))
67 (byte-equal head (byte 9)))
68 zero)))))
69 digits)
70 zero))
71
72def magnitudeSuccessor =
73 (lambda unrestricted digits : Bytes . (magnitudeSuccessorDigits (magnitudeNormalize digits)))
74
75def magnitudePredecessor =
76 (lambda unrestricted digits : Bytes .
77 (magnitudeNormalize
78 (app
79 (bytes-eliminate
80 (lambda unrestricted rest : Bytes . (pi unrestricted force : Nat . Bytes))
81 (lambda unrestricted force : Nat . b"")
82 (lambda unrestricted head : Byte .
83 (lambda unrestricted tail : Bytes .
84 (lambda unrestricted continue : (pi unrestricted force : Nat . Bytes) .
85 (lambda unrestricted force : Nat .
86 (app
87 (nat-eliminate
88 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
89 (lambda unrestricted force : Nat .
90 (bytes-cons
91 (nat-to-byte
92 (Std.Natural/naturalSaturatingSubtract (byte-to-nat head) (succ zero)))
93 tail))
94 (lambda unrestricted predecessor : Nat .
95 (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
96 (lambda unrestricted force : Nat . (bytes-cons (byte 9) (continue zero)))))
97 (byte-equal head (byte 0)))
98 zero)))))
99 (magnitudeNormalize digits))
100 zero)))
101
102def magnitudeFromNatural =
103 (lambda unrestricted value : Nat .
104 (nat-eliminate
105 (lambda unrestricted count : Nat . Bytes)
106 b""
107 (lambda unrestricted predecessor : Nat .
108 (lambda unrestricted digits : Bytes . (magnitudeSuccessorDigits digits)))
109 value))
110
111-- Evaluate decimal digits modulo 256 without constructing the whole natural.
112def magnitudeByteDouble =
113 (lambda unrestricted value : Byte .
114 (nat-to-byte (Std.Natural/naturalAdd (byte-to-nat value) (byte-to-nat value))))
115
116def magnitudeLowByte =
117 (lambda unrestricted digits : Bytes .
118 (bytes-eliminate
119 (lambda unrestricted rest : Bytes . Byte)
120 (byte 0)
121 (lambda unrestricted head : Byte .
122 (lambda unrestricted tail : Bytes .
123 (lambda unrestricted continue : Byte .
124 (nat-to-byte
125 (Std.Natural/naturalAdd
126 (byte-to-nat head)
127 (Std.Natural/naturalAdd
128 (byte-to-nat (magnitudeByteDouble continue))
129 (byte-to-nat
130 (magnitudeByteDouble (magnitudeByteDouble (magnitudeByteDouble continue))))))))))
131 digits))
132
133def magnitudeCompareSameLength =
134 (lambda unrestricted left : Bytes .
135 (lambda unrestricted right : Bytes .
136 (app
137 (bytes-eliminate
138 (lambda unrestricted rest : Bytes . (pi unrestricted right : Bytes . Nat))
139 (lambda unrestricted right : Bytes .
140 (app
141 (nat-eliminate
142 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Nat))
143 (lambda unrestricted force : Nat . (succ zero))
144 (lambda unrestricted predecessor : Nat .
145 (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
146 (lambda unrestricted force : Nat . zero)))
147 (bytes-equal right b""))
148 zero))
149 (lambda unrestricted head : Byte .
150 (lambda unrestricted tail : Bytes .
151 (lambda unrestricted continue : (pi unrestricted right : Bytes . Nat) .
152 (lambda unrestricted right : Bytes .
153 (app
154 (nat-eliminate
155 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Nat))
156 (lambda unrestricted force : Nat .
157 (app
158 (lambda unrestricted higher : Nat .
159 (app
160 (nat-eliminate
161 (lambda unrestricted flag : Nat .
162 (pi unrestricted force : Nat . Nat))
163 (lambda unrestricted force : Nat . higher)
164 (lambda unrestricted predecessor : Nat .
165 (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
166 (lambda unrestricted force : Nat .
167 (app
168 (nat-eliminate
169 (lambda unrestricted flag : Nat .
170 (pi unrestricted force : Nat . Nat))
171 (lambda unrestricted force : Nat .
172 (app
173 (nat-eliminate
174 (lambda unrestricted flag : Nat .
175 (pi unrestricted force : Nat . Nat))
176 (lambda unrestricted force : Nat . (succ (succ zero)))
177 (lambda unrestricted predecessor : Nat .
178 (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
179 (lambda unrestricted force : Nat . zero)))
180 (byte-equal head (bytes-head right)))
181 zero))
182 (lambda unrestricted predecessor : Nat .
183 (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
184 (lambda unrestricted force : Nat . (succ zero))))
185 (nat-less-than
186 (byte-to-nat head)
187 (byte-to-nat (bytes-head right))))
188 zero))))
189 (Std.Natural/naturalIsZero higher))
190 zero))
191 (continue (bytes-tail right))))
192 (lambda unrestricted predecessor : Nat .
193 (lambda unrestricted induction : (pi unrestricted force : Nat . Nat) .
194 (lambda unrestricted force : Nat . (succ (succ zero)))))
195 (bytes-equal right b""))
196 zero)))))
197 left)
198 right)))
199
200-- Internal canonical comparison can decide unequal digit lengths immediately.
201-- 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)))
223
224def magnitudeCompare =
225 (lambda unrestricted left : Bytes .
226 (lambda unrestricted right : Bytes .
227 (magnitudeCompareCanonical (magnitudeNormalize left) (magnitudeNormalize right))))
228
229def magnitudeLessCanonical =
230 (lambda unrestricted left : Bytes .
231 (lambda unrestricted right : Bytes .
232 (Std.Natural/naturalEqual (magnitudeCompareCanonical left right) (succ zero))))
233
234def magnitudeLess =
235 (lambda unrestricted left : Bytes .
236 (lambda unrestricted right : Bytes .
237 (Std.Natural/naturalEqual (magnitudeCompare left right) (succ zero))))
238
239def magnitudeAdd =
240 (lambda unrestricted left : Bytes .
241 (lambda unrestricted right : Bytes .
242 (bytes-builder-build
243 (app
244 (bytes-eliminate
245 (lambda unrestricted rest : Bytes .
246 (pi unrestricted right : Bytes . (pi unrestricted carry : Nat . BytesBuilder)))
247 (lambda unrestricted right : Bytes .
248 (lambda unrestricted carry : Nat .
249 (bytes-builder-chunk
250 (app
251 (nat-eliminate
252 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
253 (lambda unrestricted force : Nat . right)
254 (lambda unrestricted predecessor : Nat .
255 (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
256 (lambda unrestricted force : Nat . (magnitudeSuccessorDigits right))))
257 carry)
258 zero))))
259 (lambda unrestricted head : Byte .
260 (lambda unrestricted tail : Bytes .
261 (lambda unrestricted continue : (pi unrestricted right : Bytes . (pi unrestricted carry : Nat . BytesBuilder)) .
262 (lambda unrestricted right : Bytes .
263 (lambda unrestricted carry : Nat .
264 (app
265 (lambda unrestricted total : Nat .
266 (app
267 (nat-eliminate
268 (lambda unrestricted flag : Nat .
269 (pi unrestricted force : Nat . BytesBuilder))
270 (lambda unrestricted force : Nat .
271 (bytes-builder-append
272 (bytes-builder-chunk
273 (bytes-cons
274 (nat-to-byte
275 (Std.Natural/naturalAdd total (byte-to-nat (byte 246))))
276 b""))
277 (continue (bytes-tail right) (succ zero))))
278 (lambda unrestricted predecessor : Nat .
279 (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
280 (lambda unrestricted force : Nat .
281 (bytes-builder-append
282 (bytes-builder-chunk (bytes-cons (nat-to-byte total) b""))
283 (continue (bytes-tail right) zero)))))
284 (nat-less-than total (byte-to-nat (byte 10))))
285 zero))
286 (Std.Natural/naturalAdd
287 carry
288 (Std.Natural/naturalAdd
289 (byte-to-nat head)
290 (byte-to-nat (bytes-head right))))))))))
291 left)
292 right
293 zero))))
294
295-- Saturating subtraction over canonical digits. Compare before borrowing so
296-- underflow produces canonical zero. All Nat arithmetic is bounded to 0..19;
297-- the numeric value is never expanded to a unary natural.
298def magnitudeSubtractBorrow =
299 (lambda unrestricted digit : Byte .
300 (lambda unrestricted subtrahend : Nat . (nat-less-than (byte-to-nat digit) subtrahend)))
301
302def magnitudeSubtractDigit =
303 (lambda unrestricted digit : Byte .
304 (lambda unrestricted subtrahend : Nat .
305 (lambda unrestricted borrow : Nat .
306 (nat-to-byte
307 (Std.Natural/naturalSaturatingSubtract
308 (Std.Natural/naturalAdd
309 (byte-to-nat digit)
310 (Std.Natural/naturalMultiply borrow (byte-to-nat (byte 10))))
311 subtrahend)))))
312
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)))))
344
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)))
357
358-- Decimal long division: with remainder < divisor, bringing down one digit
359-- makes the next quotient digit at most nine. The bounded digit loop never
360-- iterates a number of times proportional to the dividend's numeric value.
361def magnitudeDivideDigit =
362 (lambda unrestricted divisor : Bytes .
363 (lambda unrestricted dividend : Bytes .
364 (app
365 (nat-eliminate
366 (lambda unrestricted count : Nat .
367 (pi unrestricted state : (sigma unrestricted quotient : Nat . Bytes) .
368 (sigma unrestricted quotient : Nat . Bytes)))
369 (lambda unrestricted state : (sigma unrestricted quotient : Nat . Bytes) . state)
370 (lambda unrestricted predecessor : Nat .
371 (lambda unrestricted continue : (pi unrestricted state : (sigma unrestricted quotient : Nat . Bytes) . (sigma unrestricted quotient : Nat . Bytes)) .
372 (lambda unrestricted state : (sigma unrestricted quotient : Nat . Bytes) .
373 (app
374 (nat-eliminate
375 (lambda unrestricted smaller : Nat .
376 (pi unrestricted force : Nat . (sigma unrestricted quotient : Nat . Bytes)))
377 (lambda unrestricted force : Nat .
378 (continue
379 (pair
380 (sigma unrestricted quotient : Nat . Bytes)
381 (succ (first state))
382 (magnitudeSubtractOrdered (second state) divisor))))
383 (lambda unrestricted unused : Nat .
384 (lambda unrestricted ignored : (pi unrestricted force : Nat . (sigma unrestricted quotient : Nat . Bytes)) .
385 (lambda unrestricted force : Nat . state)))
386 (magnitudeLessCanonical (second state) divisor))
387 zero))))
388 (byte-to-nat (byte 9)))
389 (pair (sigma unrestricted quotient : Nat . Bytes) zero dividend))))
390
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))))))))
404
405def magnitudeDivModNonzero =
406 (lambda unrestricted dividend : Bytes .
407 (lambda unrestricted divisor : Bytes .
408 (app
409 (lambda unrestricted result : (sigma unrestricted quotient : BytesBuilder . Bytes) .
410 (pair
411 (sigma unrestricted quotient : Bytes . Bytes)
412 (magnitudeNormalize (bytes-builder-build (first result)))
413 (second result)))
414 (bytes-eliminate
415 (lambda unrestricted rest : Bytes . (sigma unrestricted quotient : BytesBuilder . Bytes))
416 (pair (sigma unrestricted quotient : BytesBuilder . Bytes) (bytes-builder-empty) b"")
417 (lambda unrestricted head : Byte .
418 (lambda unrestricted tail : Bytes .
419 (lambda unrestricted prefix : (sigma unrestricted quotient : BytesBuilder . Bytes) .
420 (magnitudeDivideStep divisor head prefix))))
421 dividend))))
422
423-- Same total convention as the compile-time core: x/0 = 0, x mod 0 = x.
424-- Inputs use the canonical internal representation; the checked owner admits
425-- external digits before entering this arithmetic layer.
426def magnitudeDivMod =
427 (lambda unrestricted dividend : Bytes .
428 (lambda unrestricted divisor : Bytes .
429 (app
430 (nat-eliminate
431 (lambda unrestricted isZero : Nat .
432 (pi unrestricted force : Nat . (sigma unrestricted quotient : Bytes . Bytes)))
433 (lambda unrestricted force : Nat . (magnitudeDivModNonzero dividend divisor))
434 (lambda unrestricted predecessor : Nat .
435 (lambda unrestricted induction : (pi unrestricted force : Nat . (sigma unrestricted quotient : Bytes . Bytes)) .
436 (lambda unrestricted force : Nat .
437 (pair (sigma unrestricted quotient : Bytes . Bytes) b"" dividend))))
438 (bytes-equal divisor b""))
439 zero)))
440
441def magnitudeDivide =
442 (lambda unrestricted dividend : Bytes .
443 (lambda unrestricted divisor : Bytes . (first (magnitudeDivMod dividend divisor))))
444
445def magnitudeModulo =
446 (lambda unrestricted dividend : Bytes .
447 (lambda unrestricted divisor : Bytes . (second (magnitudeDivMod dividend divisor))))
448
449def magnitudeDouble =
450 (lambda unrestricted digits : Bytes .
451 (bytes-builder-build
452 (app
453 (bytes-eliminate
454 (lambda unrestricted rest : Bytes . (pi unrestricted carry : Nat . BytesBuilder))
455 (lambda unrestricted carry : Nat .
456 (app
457 (nat-eliminate
458 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . BytesBuilder))
459 (lambda unrestricted force : Nat . (bytes-builder-empty))
460 (lambda unrestricted predecessor : Nat .
461 (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
462 (lambda unrestricted force : Nat .
463 (bytes-builder-chunk (bytes-cons (byte 1) b"")))))
464 carry)
465 zero))
466 (lambda unrestricted head : Byte .
467 (lambda unrestricted tail : Bytes .
468 (lambda unrestricted continue : (pi unrestricted carry : Nat . BytesBuilder) .
469 (lambda unrestricted carry : Nat .
470 (app
471 (nat-eliminate
472 (lambda unrestricted flag : Nat .
473 (pi unrestricted force : Nat . BytesBuilder))
474 (lambda unrestricted force : Nat .
475 (app
476 (lambda unrestricted reduced : Nat .
477 (bytes-builder-append
478 (bytes-builder-chunk
479 (bytes-cons
480 (nat-to-byte
481 (Std.Natural/naturalAdd
482 carry
483 (Std.Natural/naturalAdd reduced reduced)))
484 b""))
485 (continue (succ zero))))
486 (byte-to-nat
487 (nat-to-byte
488 (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat (byte 251)))))))
489 (lambda unrestricted predecessor : Nat .
490 (lambda unrestricted induction : (pi unrestricted force : Nat . BytesBuilder) .
491 (lambda unrestricted force : Nat .
492 (bytes-builder-append
493 (bytes-builder-chunk
494 (bytes-cons
495 (nat-to-byte
496 (Std.Natural/naturalAdd
497 carry
498 (Std.Natural/naturalAdd (byte-to-nat head) (byte-to-nat head))))
499 b""))
500 (continue zero)))))
501 (byte-less-than head (byte 5)))
502 zero)))))
503 digits)
504 zero)))
505
506def magnitudeMultiplyDigit =
507 (lambda unrestricted digits : Bytes .
508 (lambda unrestricted factor : Byte .
509 (magnitudeNormalize
510 (app
511 (bytes-eliminate
512 (lambda unrestricted rest : Bytes . (pi unrestricted carry : Nat . Bytes))
513 (lambda unrestricted carry : Nat . (magnitudeFromNatural carry))
514 (lambda unrestricted head : Byte .
515 (lambda unrestricted tail : Bytes .
516 (lambda unrestricted continue : (pi unrestricted carry : Nat . Bytes) .
517 (lambda unrestricted carry : Nat .
518 (app
519 (lambda unrestricted total : Nat .
520 (app
521 (lambda unrestricted nextCarry : Nat .
522 (bytes-cons
523 (nat-to-byte
524 (Std.Natural/naturalSaturatingSubtract
525 total
526 (Std.Natural/naturalMultiply nextCarry (byte-to-nat (byte 10)))))
527 (continue nextCarry)))
528 (Std.Natural/naturalDivideUnchecked total (byte-to-nat (byte 10)))))
529 (Std.Natural/naturalAdd
530 (Std.Natural/naturalMultiply (byte-to-nat head) (byte-to-nat factor))
531 carry))))))
532 digits)
533 zero))))
534
535def magnitudeMultiply =
536 (lambda unrestricted left : Bytes .
537 (lambda unrestricted right : Bytes .
538 (bytes-eliminate
539 (lambda unrestricted rest : Bytes . Bytes)
540 b""
541 (lambda unrestricted head : Byte .
542 (lambda unrestricted tail : Bytes .
543 (lambda unrestricted continue : Bytes .
544 (magnitudeAdd
545 (magnitudeMultiplyDigit left head)
546 (app
547 (nat-eliminate
548 (lambda unrestricted flag : Nat . (pi unrestricted force : Nat . Bytes))
549 (lambda unrestricted force : Nat . (bytes-cons (byte 0) continue))
550 (lambda unrestricted predecessor : Nat .
551 (lambda unrestricted induction : (pi unrestricted force : Nat . Bytes) .
552 (lambda unrestricted force : Nat . b"")))
553 (bytes-equal continue b""))
554 zero)))))
555 right)))
556
557def magnitudeRepeatSmall =
558 (lambda erased State : Type 0 .
559 (lambda unrestricted count : Nat .
560 (lambda unrestricted step : (pi unrestricted value : State . State) .
561 (lambda unrestricted seed : State .
562 (nat-eliminate
563 (lambda unrestricted index : Nat . State)
564 seed
565 (lambda unrestricted predecessor : Nat .
566 (lambda unrestricted induction : State . (step induction)))
567 count)))))
568
569def magnitudeIterate =
570 (lambda erased State : Type 0 .
571 (lambda unrestricted digits : Bytes .
572 (lambda unrestricted step : (pi unrestricted value : State . State) .
573 (lambda unrestricted seed : State .
574 (app
575 (bytes-eliminate
576 (lambda unrestricted rest : Bytes .
577 (pi unrestricted step : (pi unrestricted value : State . State) .
578 (pi unrestricted seed : State . State)))
579 (lambda unrestricted step : (pi unrestricted value : State . State) .
580 (lambda unrestricted seed : State . seed))
581 (lambda unrestricted head : Byte .
582 (lambda unrestricted tail : Bytes .
583 (lambda unrestricted continue : (pi unrestricted step : (pi unrestricted value : State . State) . (pi unrestricted seed : State . State)) .
584 (lambda unrestricted step : (pi unrestricted value : State . State) .
585 (lambda unrestricted seed : State .
586 (continue
587 (lambda unrestricted state : State .
588 (magnitudeRepeatSmall State (byte-to-nat (byte 10)) step state))
589 (magnitudeRepeatSmall State (byte-to-nat head) step seed)))))))
590 digits)
591 step
592 seed)))))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.