One first-order digit-take step over the `JSONDigitSplit` accumulator.
The head is peeked with the O(1) `bytes-head` view (not the tail-forcing
`bytes-eliminate`): a digit is appended to the builder and the remaining
advances; a non-digit or the empty string is a fixed point (the accumulator is
returned unchanged, so `remaining` keeps pointing at the first non-digit and
every later step is a no-op). Digits are appended front-to-back, matching the
original's head-first prepend.
883def jsonTakeDigitsStep =
884 (lambda unrestricted acc : (family JSONDigitSplit) .
885 (eliminate
886 JSONDigitSplit
887 (lambda unrestricted current : (family JSONDigitSplit) . (family JSONDigitSplit))
888 acc
889 (branch
890 JSONDigitSplitValue
891 builder
892 remaining
893 count
894 .
895 (nat-eliminate
896 (lambda unrestricted nonEmpty : Nat . (family JSONDigitSplit))
897 (app
898 (lambda unrestricted head : Byte .
899 (nat-eliminate
900 (lambda unrestricted digit : Nat . (family JSONDigitSplit))
901 acc
902 (lambda unrestricted digitPredecessor : Nat .
903 (lambda unrestricted digitInduction : (family JSONDigitSplit) .
904 (constructor
905 JSONDigitSplit
906 JSONDigitSplitValue
907 (bytes-builder-append builder (bytes-builder-chunk (bytes-cons head b"")))
908 (bytes-tail remaining)
909 (succ count))))
910 (jsonByteIsDigit head)))
911 (bytes-head remaining))
912 (lambda unrestricted emptyPredecessor : Nat .
913 (lambda unrestricted emptyInduction : (family JSONDigitSplit) . acc))
914 (naturalIsZero (bytes-length remaining))))))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.