Field projection for `sha256DigestTelemetryShifts`, generated from the declaration: the family
has one constructor, so this is the unique total projection.
386def sha256DigestTelemetryShifts =
387 (lambda unrestricted value : (family SHA256DigestTelemetry) .
388 (eliminate
389 SHA256DigestTelemetry
390 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
391 value
392 (branch
393 SHA256DigestTelemetryValue
394 sha256DigestTelemetryInputBytes
395 sha256DigestTelemetryPaddedBytes
396 sha256DigestTelemetryBlocks
397 sha256DigestTelemetryDecodedWords
398 sha256DigestTelemetryExpandedWords
399 sha256DigestTelemetryRounds
400 sha256DigestTelemetryLookups
401 sha256DigestTelemetrySigmas
402 sha256DigestTelemetryRotates
403 sha256DigestTelemetryShifts
404 sha256DigestTelemetryBooleans
405 sha256DigestTelemetryAdds
406 .
407 sha256DigestTelemetryShifts)))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.