963def jsonIntegerDigitsFitInt64 =
964 (lambda unrestricted digits : Bytes .
965 (nat-eliminate
966 (lambda unrestricted current : Nat . Nat)
967 (nat-eliminate
968 (lambda unrestricted current : Nat . Nat)
969 (eliminate
970 DataBytesOrdering
971 (lambda unrestricted current : (family DataBytesOrdering) . Nat)
972 (dataBytesCompare digits jsonInt64MaximumDigits)
973 (branch DataBytesLess . (succ zero))
974 (branch DataBytesEqual . (succ zero))
975 (branch DataBytesGreater . zero))
976 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . zero))
977 (naturalSaturatingSubtract (bytes-length digits) (bytes-length jsonInt64MaximumDigits)))
978 (lambda unrestricted predecessor : Nat . (lambda unrestricted induction : Nat . (succ zero)))
979 (naturalSaturatingSubtract (bytes-length jsonInt64MaximumDigits) (bytes-length 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.