1499def jsonParseArrayValuesStep =
1500 (lambda unrestricted parser : (family JSONParser) .
1501 (lambda unrestricted input : Bytes .
1502 (app
1503 (lambda unrestricted clean : Bytes .
1504 (nat-eliminate
1505 (lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
1506 (app
1507 (lambda unrestricted head : Byte .
1508 (app
1509 (lambda unrestricted tail : Bytes .
1510 (nat-eliminate
1511 (lambda unrestricted closed : Nat . (family JSONParseResult))
1512 (eliminate
1513 JSONParseResult
1514 (lambda unrestricted current : (family JSONParseResult) .
1515 (family JSONParseResult))
1516 (jsonParserValue parser clean)
1517 (branch
1518 JSONParsed
1519 value
1520 afterValue
1521 .
1522 (app
1523 (lambda unrestricted delimiterInput : Bytes .
1524 (nat-eliminate
1525 (lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
1526 (jsonParseArrayValuesStepPart1
1527 parser
1528 value
1529 delimiterInput
1530 (bytes-head delimiterInput)
1531 (bytes-tail delimiterInput)
1532 (jsonParseFailure
1533 (constructor JSONErrorCode JSONArrayDelimiterMissing)
1534 delimiterInput))
1535 (lambda unrestricted emptyPredecessor : Nat .
1536 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1537 (jsonParseFailure
1538 (constructor JSONErrorCode JSONArrayDelimiterMissing)
1539 delimiterInput)))
1540 (naturalIsZero (bytes-length delimiterInput))))
1541 (jsonDropWhitespace afterValue)))
1542 (branch JSONParseFailed code remaining . (jsonParseFailure code remaining)))
1543 (lambda unrestricted closePredecessor : Nat .
1544 (lambda unrestricted closeInduction : (family JSONParseResult) .
1545 (constructor
1546 JSONParseResult
1547 JSONParsed
1548 (constructor JSON JSONArrayEnd)
1549 tail)))
1550 (byte-equal head (byte 93))))
1551 (bytes-tail clean)))
1552 (bytes-head clean))
1553 (lambda unrestricted emptyPredecessor : Nat .
1554 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1555 (jsonParseFailure (constructor JSONErrorCode JSONUnexpectedEnd) clean)))
1556 (naturalIsZero (bytes-length clean))))
1557 (jsonDropWhitespace input))))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.