1585def checkpointValidateSchemaVersion =
1586 (lambda unrestricted declared : Bytes .
1587 (nat-eliminate
1588 (lambda unrestricted matched : Nat . (family CheckpointSchemaIdentityResult))
1589 (constructor
1590 CheckpointSchemaIdentityResult
1591 CheckpointSchemaIdentityRejected
1592 (checkpointFailure
1593 (constructor CheckpointErrorCode CheckpointSchemaVersionUnsupported)
1594 zero
1595 checkpointSchemaVersion
1596 declared)
1597 (bytes-length declared))
1598 (lambda unrestricted predecessor : Nat .
1599 (lambda unrestricted induction : (family CheckpointSchemaIdentityResult) .
1600 (constructor
1601 CheckpointSchemaIdentityResult
1602 CheckpointSchemaIdentityAccepted
1603 (bytes-length declared))))
1604 (bytes-equal declared checkpointSchemaVersion)))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.