Field projection for `sha256DigestTelemetryAdds`, generated from the declaration: the family
has one constructor, so this is the unique total projection.
161def sha256DigestTelemetryAdds =
162 (lambda unrestricted value : (family SHA256DigestTelemetry) .
163 (eliminate
164 SHA256DigestTelemetry
165 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
166 value
167 (branch
168 SHA256DigestTelemetryValue
169 sha256DigestTelemetryInputBytes
170 sha256DigestTelemetryPaddedBytes
171 sha256DigestTelemetryBlocks
172 sha256DigestTelemetryDecodedWords
173 sha256DigestTelemetryExpandedWords
174 sha256DigestTelemetryRounds
175 sha256DigestTelemetryLookups
176 sha256DigestTelemetrySigmas
177 sha256DigestTelemetryRotates
178 sha256DigestTelemetryShifts
179 sha256DigestTelemetryBooleans
180 sha256DigestTelemetryAdds
181 .
182 sha256DigestTelemetryAdds)))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.