439def telemetryRecordPartsAdmission =
440 (lambda unrestricted parts : (family TelemetryRecordParts) .
441 (eliminate
442 TelemetryRecordParts
443 (lambda unrestricted current : (family TelemetryRecordParts) . Nat)
444 parts
445 (branch TelemetryRecordEnd . 1)
446 (branch TelemetryRecordLiteral bytes tail induction . induction)
447 (branch
448 TelemetryRecordDecimal
449 signed
450 offset
451 tail
452 induction
453 .
454 (naturalAnd
455 induction
456 (naturalAnd
457 (naturalLessOrEqual signed 1)
458 (naturalIsZero
459 (telemetryWordCellAdmission offset captureRecordBytes telemetryDecimalCellBytes)))))
460 (branch
461 TelemetryRecordHex
462 source
463 offset
464 width
465 reverse
466 nonzero
467 tail
468 induction
469 .
470 (naturalAnd
471 induction
472 (naturalAnd
473 (naturalLessOrEqual source 1)
474 (naturalAnd
475 (naturalLessOrEqual nonzero 1)
476 (naturalAnd
477 (aosChoose Nat nonzero (naturalEqual width telemetryIdentityBytes) 1)
478 (naturalIsZero
479 (telemetryHexSliceCellAdmission
480 width
481 reverse
482 offset
483 (aosChoose Nat source telemetryIdentitySetBytes captureRecordBytes)
484 (telemetryHexCellBytes telemetryHexSourceMaximumBytes))))))))))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.