1173def jsonWord64Digits =
1174 (lambda unrestricted digits : Bytes .
1175 (app
1176 (bytes-eliminate
1177 (lambda unrestricted current : Bytes .
1178 (pi unrestricted accumulator : (family ModelWord64) . (family JSONWord64AccessResult)))
1179 (lambda unrestricted accumulator : (family ModelWord64) .
1180 (constructor JSONWord64AccessResult JSONWord64AccessSucceeded accumulator))
1181 (lambda unrestricted head : Byte .
1182 (lambda unrestricted tail : Bytes .
1183 (lambda unrestricted induction : (pi unrestricted accumulator : (family ModelWord64) . (family JSONWord64AccessResult)) .
1184 (lambda unrestricted accumulator : (family ModelWord64) .
1185 (nat-eliminate
1186 (lambda unrestricted valid : Nat . (family JSONWord64AccessResult))
1187 (constructor JSONWord64AccessResult JSONWord64AccessFailed
1188 (constructor JSONErrorCode JSONExpectedInteger))
1189 (lambda unrestricted p : Nat .
1190 (lambda unrestricted unused : (family JSONWord64AccessResult) .
1191 (induction (jsonWord64DigitStep accumulator head))))
1192 (jsonByteIsDigit head))))))
1193 digits)
1194 modelWord64Zero))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.