Field projection (fields do not create definitions).
435def sha256DigestTelemetryBlocks =
436 (lambda unrestricted value : (family SHA256DigestTelemetry) .
437 (eliminate
438 SHA256DigestTelemetry
439 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
440 value
441 (branch
442 SHA256DigestTelemetryValue
443 sha256DigestTelemetryInputBytes
444 sha256DigestTelemetryPaddedBytes
445 sha256DigestTelemetryBlocksField
446 sha256DigestTelemetryDecodedWords
447 sha256DigestTelemetryExpandedWords
448 sha256DigestTelemetryRounds
449 sha256DigestTelemetryLookups
450 sha256DigestTelemetrySigmas
451 sha256DigestTelemetryRotates
452 sha256DigestTelemetryShifts
453 sha256DigestTelemetryBooleans
454 sha256DigestTelemetryAdds
455 .
456 sha256DigestTelemetryBlocksField)))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.