Field projection for `sha256DigestTelemetryExpandedWords`, generated from the declaration: the family
has one constructor, so this is the unique total projection.
236def sha256DigestTelemetryExpandedWords =
237 (lambda unrestricted value : (family SHA256DigestTelemetry) .
238 (eliminate
239 SHA256DigestTelemetry
240 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
241 value
242 (branch
243 SHA256DigestTelemetryValue
244 sha256DigestTelemetryInputBytes
245 sha256DigestTelemetryPaddedBytes
246 sha256DigestTelemetryBlocks
247 sha256DigestTelemetryDecodedWords
248 sha256DigestTelemetryExpandedWords
249 sha256DigestTelemetryRounds
250 sha256DigestTelemetryLookups
251 sha256DigestTelemetrySigmas
252 sha256DigestTelemetryRotates
253 sha256DigestTelemetryShifts
254 sha256DigestTelemetryBooleans
255 sha256DigestTelemetryAdds
256 .
257 sha256DigestTelemetryExpandedWords)))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.