536def sha256DigestTelemetryCombine =
537 (lambda unrestricted inputBytes : Nat .
538 (lambda unrestricted paddedBytes : Nat .
539 (lambda unrestricted left : (family SHA256DigestTelemetry) .
540 (lambda unrestricted right : (family SHA256DigestTelemetry) .
541 (eliminate
542 SHA256DigestTelemetry
543 (lambda unrestricted current : (family SHA256DigestTelemetry) .
544 (family SHA256DigestTelemetry))
545 left
546 (branch
547 SHA256DigestTelemetryValue
548 leftInput
549 leftPadded
550 leftBlocks
551 leftDecoded
552 leftExpanded
553 leftRounds
554 leftLookups
555 leftSigmas
556 leftRotates
557 leftShifts
558 leftBooleans
559 leftAdds
560 .
561 (eliminate
562 SHA256DigestTelemetry
563 (lambda unrestricted current : (family SHA256DigestTelemetry) .
564 (family SHA256DigestTelemetry))
565 right
566 (branch
567 SHA256DigestTelemetryValue
568 rightInput
569 rightPadded
570 rightBlocks
571 rightDecoded
572 rightExpanded
573 rightRounds
574 rightLookups
575 rightSigmas
576 rightRotates
577 rightShifts
578 rightBooleans
579 rightAdds
580 .
581 (constructor
582 SHA256DigestTelemetry
583 SHA256DigestTelemetryValue
584 inputBytes
585 paddedBytes
586 (naturalAdd leftBlocks rightBlocks)
587 (naturalAdd leftDecoded rightDecoded)
588 (naturalAdd leftExpanded rightExpanded)
589 (naturalAdd leftRounds rightRounds)
590 (naturalAdd leftLookups rightLookups)
591 (naturalAdd leftSigmas rightSigmas)
592 (naturalAdd leftRotates rightRotates)
593 (naturalAdd leftShifts rightShifts)
594 (naturalAdd leftBooleans rightBooleans)
595 (naturalAdd leftAdds rightAdds))))))))))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.