Field projection for `sha256DigestTelemetryRotates`, generated from the declaration: the family
has one constructor, so this is the unique total projection.
336def sha256DigestTelemetryRotates =
337 (lambda unrestricted value : (family SHA256DigestTelemetry) .
338 (eliminate
339 SHA256DigestTelemetry
340 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
341 value
342 (branch
343 SHA256DigestTelemetryValue
344 sha256DigestTelemetryInputBytes
345 sha256DigestTelemetryPaddedBytes
346 sha256DigestTelemetryBlocks
347 sha256DigestTelemetryDecodedWords
348 sha256DigestTelemetryExpandedWords
349 sha256DigestTelemetryRounds
350 sha256DigestTelemetryLookups
351 sha256DigestTelemetrySigmas
352 sha256DigestTelemetryRotates
353 sha256DigestTelemetryShifts
354 sha256DigestTelemetryBooleans
355 sha256DigestTelemetryAdds
356 .
357 sha256DigestTelemetryRotates)))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.