Field projection for `sha256DigestTelemetryDecodedWords`, generated from the declaration: the family
has one constructor, so this is the unique total projection.
211def sha256DigestTelemetryDecodedWords =
212 (lambda unrestricted value : (family SHA256DigestTelemetry) .
213 (eliminate
214 SHA256DigestTelemetry
215 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
216 value
217 (branch
218 SHA256DigestTelemetryValue
219 sha256DigestTelemetryInputBytes
220 sha256DigestTelemetryPaddedBytes
221 sha256DigestTelemetryBlocks
222 sha256DigestTelemetryDecodedWords
223 sha256DigestTelemetryExpandedWords
224 sha256DigestTelemetryRounds
225 sha256DigestTelemetryLookups
226 sha256DigestTelemetrySigmas
227 sha256DigestTelemetryRotates
228 sha256DigestTelemetryShifts
229 sha256DigestTelemetryBooleans
230 sha256DigestTelemetryAdds
231 .
232 sha256DigestTelemetryDecodedWords)))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.