467def publicationTypedIdentitiesValid =
468 (lambda unrestricted identities : Bytes .
469 (naturalAnd
470 (naturalEqual (bytes-length identities) telemetryIdentitySetBytes)
471 (nat-eliminate
472 (lambda unrestricted current : Nat . Nat)
473 1
474 (lambda unrestricted index : Nat .
475 (lambda unrestricted induction : Nat .
476 (naturalAnd
477 induction
478 (telemetryBinaryIdentityValid
479 (dataBytesTakeValidated
480 telemetryIdentityBytes
481 (dataBytesDropValidated (telemetryIdentityOffset index) identities))))))
482 (succ telemetryProducerEpochIndex))))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.