607def integerLiteralStripSeparators =
608 (lambda unrestricted digits : Bytes .
609 (bytes-eliminate
610 (lambda unrestricted remaining : Bytes . Bytes)
611 b""
612 (lambda unrestricted head : Byte .
613 (lambda unrestricted tail : Bytes .
614 (lambda unrestricted slots : Bytes .
615 (nat-eliminate
616 (lambda unrestricted current : Nat . Bytes)
617 (bytes-cons head slots)
618 (lambda unrestricted predecessor : Nat .
619 (lambda unrestricted induction : Bytes . slots))
620 (byte-equal head (byte 95))))))
621 digits))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.