Source/Packages

Data.SHA256Digest

packages/foundation/standard/src/Data/SHA256Digest.alpha

1,631 lines150 declarations64.2 KiBSHA-256 c46a79f2ab9a

def · lines 311–332

sha256DigestTelemetryPaddedBytes

Full file
Field projection for `sha256DigestTelemetryPaddedBytes`, generated from the declaration: the family has one constructor, so this is the unique total projection.
311def sha256DigestTelemetryPaddedBytes =
312  (lambda unrestricted value : (family SHA256DigestTelemetry) .
313    (eliminate
314      SHA256DigestTelemetry
315      (lambda unrestricted current : (family SHA256DigestTelemetry) . Nat)
316      value
317      (branch
318        SHA256DigestTelemetryValue
319        sha256DigestTelemetryInputBytes
320        sha256DigestTelemetryPaddedBytes
321        sha256DigestTelemetryBlocks
322        sha256DigestTelemetryDecodedWords
323        sha256DigestTelemetryExpandedWords
324        sha256DigestTelemetryRounds
325        sha256DigestTelemetryLookups
326        sha256DigestTelemetrySigmas
327        sha256DigestTelemetryRotates
328        sha256DigestTelemetryShifts
329        sha256DigestTelemetryBooleans
330        sha256DigestTelemetryAdds
331        .
332        sha256DigestTelemetryPaddedBytes)))

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.