the value of a string of decimal digits, most significant first (a left
fold: the accumulator is threaded through the right fold's functions)
111def aosDigitsValue =
112 (lambda unrestricted input : Bytes .
113 (app (bytes-eliminate (lambda unrestricted current : Bytes . (pi unrestricted acc : Nat . Nat))
114 (lambda unrestricted acc : Nat . acc)
115 (lambda unrestricted head : Byte . (lambda unrestricted tail : Bytes .
116 (lambda unrestricted induction : (pi unrestricted acc : Nat . Nat) .
117 (lambda unrestricted acc : Nat .
118 (induction (naturalAdd (naturalMultiply acc 10) (naturalSaturatingSubtract (byte-to-nat head) 48)))))))
119 input)
120 0))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.