Part of `jsonParseObjectMembersStep`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
1220def jsonParseObjectMembersStepPart1 =
1221 (lambda unrestricted parser : (family JSONParser) .
1222 (lambda unrestricted key : Bytes .
1223 (lambda unrestricted value : (family JSON) .
1224 (lambda unrestricted delimiterInput : Bytes .
1225 (lambda unrestricted delimiter : Byte .
1226 (lambda unrestricted afterDelimiter : Bytes .
1227 (nat-eliminate
1228 (lambda unrestricted comma : Nat . (family JSONParseResult))
1229 (nat-eliminate
1230 (lambda unrestricted close : Nat . (family JSONParseResult))
1231 (jsonParseFailure
1232 (constructor JSONErrorCode JSONObjectDelimiterMissing)
1233 delimiterInput)
1234 (lambda unrestricted closePredecessor : Nat .
1235 (lambda unrestricted closeInduction : (family JSONParseResult) .
1236 (constructor
1237 JSONParseResult
1238 JSONParsed
1239 (constructor
1240 JSON
1241 JSONObjectMember
1242 key
1243 value
1244 (constructor JSON JSONObjectEnd))
1245 afterDelimiter)))
1246 (byte-equal delimiter (byte 125)))
1247 (lambda unrestricted commaPredecessor : Nat .
1248 (lambda unrestricted commaInduction : (family JSONParseResult) .
1249 (app
1250 (lambda unrestricted nextInput : Bytes .
1251 (nat-eliminate
1252 (lambda unrestricted nonEmpty : Nat . (family JSONParseResult))
1253 (app
1254 (lambda unrestricted nextHead : Byte .
1255 (app
1256 (lambda unrestricted nextTail : Bytes .
1257 (nat-eliminate
1258 (lambda unrestricted trailingComma : Nat .
1259 (family JSONParseResult))
1260 (eliminate
1261 JSONParseResult
1262 (lambda unrestricted current : (family JSONParseResult) .
1263 (family JSONParseResult))
1264 (jsonParserObject parser nextInput)
1265 (branch
1266 JSONParsed
1267 members
1268 remaining
1269 .
1270 (constructor
1271 JSONParseResult
1272 JSONParsed
1273 (constructor JSON JSONObjectMember key value members)
1274 remaining))
1275 (branch
1276 JSONParseFailed
1277 code
1278 remaining
1279 .
1280 (jsonParseFailure code remaining)))
1281 (lambda unrestricted trailingPredecessor : Nat .
1282 (lambda unrestricted trailingInduction : (family JSONParseResult) .
1283 (jsonParseFailure
1284 (constructor JSONErrorCode JSONObjectKeyNotString)
1285 nextInput)))
1286 (byte-equal nextHead (byte 125))))
1287 (bytes-tail nextInput)))
1288 (bytes-head nextInput))
1289 (lambda unrestricted emptyPredecessor : Nat .
1290 (lambda unrestricted emptyInduction : (family JSONParseResult) .
1291 (jsonParseFailure
1292 (constructor JSONErrorCode JSONObjectKeyNotString)
1293 nextInput)))
1294 (naturalIsZero (bytes-length nextInput))))
1295 (jsonDropWhitespace afterDelimiter))))
1296 (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.