Part of `jsonParseArrayValuesStep`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
1426def jsonParseArrayValuesStepPart1 =
1427 (lambda unrestricted parser : (family JSONParser) .
1428 (lambda unrestricted value : (family JSON) .
1429 (lambda unrestricted delimiterInput : Bytes .
1430 (lambda unrestricted delimiter : Byte .
1431 (lambda unrestricted afterDelimiter : Bytes .
1432 (lambda unrestricted afterDelimiterInduction : (family JSONParseResult) .
1433 (nat-eliminate
1434 (lambda unrestricted comma : Nat . (family JSONParseResult))
1435 (nat-eliminate
1436 (lambda unrestricted close : Nat . (family JSONParseResult))
1437 (jsonParseFailure
1438 (constructor JSONErrorCode JSONArrayDelimiterMissing)
1439 delimiterInput)
1440 (lambda unrestricted closePredecessor : Nat .
1441 (lambda unrestricted closeInduction : (family JSONParseResult) .
1442 (constructor
1443 JSONParseResult
1444 JSONParsed
1445 (constructor JSON JSONArrayNext value (constructor JSON JSONArrayEnd))
1446 afterDelimiter)))
1447 (byte-equal delimiter (byte 93)))
1448 (lambda unrestricted commaPredecessor : Nat .
1449 (lambda unrestricted commaInduction : (family JSONParseResult) .
1450 (app
1451 (lambda unrestricted nextInput : Bytes .
1452 (nat-eliminate
1453 (lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
1454 (app
1455 (lambda unrestricted nextHead : Byte .
1456 (app
1457 (lambda unrestricted nextTail : Bytes .
1458 (nat-eliminate
1459 (lambda unrestricted trailingComma : Nat .
1460 (family JSONParseResult))
1461 (eliminate
1462 JSONParseResult
1463 (lambda unrestricted current : (family JSONParseResult) .
1464 (family JSONParseResult))
1465 (jsonParserArray parser nextInput)
1466 (branch
1467 JSONParsed
1468 values
1469 remaining
1470 .
1471 (constructor
1472 JSONParseResult
1473 JSONParsed
1474 (constructor JSON JSONArrayNext value values)
1475 remaining))
1476 (branch
1477 JSONParseFailed
1478 code
1479 remaining
1480 .
1481 (jsonParseFailure code remaining)))
1482 (lambda unrestricted trailingPredecessor : Nat .
1483 (lambda unrestricted trailingInduction : (family JSONParseResult) .
1484 (jsonParseFailure
1485 (constructor JSONErrorCode JSONInvalidValue)
1486 nextInput)))
1487 (byte-equal nextHead (byte 93))))
1488 (bytes-tail nextInput)))
1489 (bytes-head nextInput))
1490 (lambda unrestricted emptyPredecessor : Nat .
1491 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1492 (jsonParseFailure
1493 (constructor JSONErrorCode JSONInvalidValue)
1494 nextInput)))
1495 (naturalIsZero (bytes-length nextInput))))
1496 (jsonDropWhitespace afterDelimiter))))
1497 (byte-equal delimiter (byte 44)))))))))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.