Field projection for `sha256DigestTelemetryInputBytes`, generated from the declaration: the family
has one constructor, so this is the unique total projection.
261def sha256DigestTelemetryInputBytes =
262 (lambda unrestricted value : (family SHA256DigestTelemetry) .
263 (eliminate
264 SHA256DigestTelemetry
265 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
266 value
267 (branch
268 SHA256DigestTelemetryValue
269 sha256DigestTelemetryInputBytes
270 sha256DigestTelemetryPaddedBytes
271 sha256DigestTelemetryBlocks
272 sha256DigestTelemetryDecodedWords
273 sha256DigestTelemetryExpandedWords
274 sha256DigestTelemetryRounds
275 sha256DigestTelemetryLookups
276 sha256DigestTelemetrySigmas
277 sha256DigestTelemetryRotates
278 sha256DigestTelemetryShifts
279 sha256DigestTelemetryBooleans
280 sha256DigestTelemetryAdds
281 .
282 sha256DigestTelemetryInputBytes)))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.