Field projection for `sha256DigestTelemetryLookups`, generated from the declaration: the family
has one constructor, so this is the unique total projection.
286def sha256DigestTelemetryLookups =
287 (lambda unrestricted value : (family SHA256DigestTelemetry) .
288 (eliminate
289 SHA256DigestTelemetry
290 (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
291 value
292 (branch
293 SHA256DigestTelemetryValue
294 sha256DigestTelemetryInputBytes
295 sha256DigestTelemetryPaddedBytes
296 sha256DigestTelemetryBlocks
297 sha256DigestTelemetryDecodedWords
298 sha256DigestTelemetryExpandedWords
299 sha256DigestTelemetryRounds
300 sha256DigestTelemetryLookups
301 sha256DigestTelemetrySigmas
302 sha256DigestTelemetryRotates
303 sha256DigestTelemetryShifts
304 sha256DigestTelemetryBooleans
305 sha256DigestTelemetryAdds
306 .
307 sha256DigestTelemetryLookups)))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.