Part of `jsonParseObjectMembersStep`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
1300def jsonParseObjectMembersStepPart2 =
1301 (lambda unrestricted parser : (family JSONParser) .
1302 (lambda unrestricted key : Bytes .
1303 (lambda unrestricted colonInput : Bytes .
1304 (lambda unrestricted colon : Byte .
1305 (lambda unrestricted afterColon : Bytes .
1306 (lambda unrestricted afterColonInduction : (family JSONParseResult) .
1307 (nat-eliminate
1308 (lambda unrestricted validColon : Nat . (family JSONParseResult))
1309 (jsonParseFailure (constructor JSONErrorCode JSONObjectColonMissing) colonInput)
1310 (lambda unrestricted colonPredecessor : Nat .
1311 (lambda unrestricted colonInduction : (family JSONParseResult) .
1312 (eliminate
1313 JSONParseResult
1314 (lambda unrestricted current : (family JSONParseResult) .
1315 (family JSONParseResult))
1316 (jsonParserValue parser afterColon)
1317 (branch
1318 JSONParsed
1319 value
1320 afterValue
1321 .
1322 (app
1323 (lambda unrestricted delimiterInput : Bytes .
1324 (nat-eliminate
1325 (lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
1326 (app
1327 (lambda unrestricted delimiter : Byte .
1328 (app
1329 (lambda unrestricted afterDelimiter : Bytes .
1330 (jsonParseObjectMembersStepPart1
1331 parser
1332 key
1333 value
1334 delimiterInput
1335 delimiter
1336 afterDelimiter))
1337 (bytes-tail delimiterInput)))
1338 (bytes-head delimiterInput))
1339 (lambda unrestricted emptyPredecessor : Nat .
1340 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1341 (jsonParseFailure
1342 (constructor JSONErrorCode JSONObjectDelimiterMissing)
1343 delimiterInput)))
1344 (naturalIsZero (bytes-length delimiterInput))))
1345 (jsonDropWhitespace afterValue)))
1346 (branch JSONParseFailed code remaining . (jsonParseFailure code remaining)))))
1347 (byte-equal colon (byte 58)))))))))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.