`groups` full groups, then the remainder group of `rest` blocks.
756def sha256DigestRunBlockGroups =
757 (lambda unrestricted groups : Nat .
758 (lambda unrestricted rest : Nat .
759 (nat-eliminate
760 (lambda unrestricted current : Nat .
761 (pi unrestricted state : (family SHA256State) .
762 (pi unrestricted input : Bytes .
763 (pi unrestricted telemetry : (family SHA256DigestTelemetry) .
764 (family SHA256DigestGroupResult)))))
765 (sha256DigestRunBlockGroup rest)
766 (lambda unrestricted predecessor : Nat .
767 (lambda unrestricted induction : (pi unrestricted state : (family SHA256State) . (pi unrestricted input : Bytes . (pi unrestricted telemetry : (family SHA256DigestTelemetry) . (family SHA256DigestGroupResult)))) .
768 (lambda unrestricted state : (family SHA256State) .
769 (lambda unrestricted input : Bytes .
770 (lambda unrestricted telemetry : (family SHA256DigestTelemetry) .
771 (eliminate
772 SHA256DigestGroupResult
773 (lambda unrestricted current : (family SHA256DigestGroupResult) .
774 (family SHA256DigestGroupResult))
775 (sha256DigestRunBlockGroup sha256DigestBlocksPerGroup state input telemetry)
776 (branch
777 SHA256DigestGroupSucceeded
778 nextState
779 remaining
780 nextTelemetry
781 .
782 (induction nextState remaining nextTelemetry))
783 (branch
784 SHA256DigestGroupFailed
785 error
786 ordinal
787 internalIndex
788 before
789 .
790 (constructor
791 SHA256DigestGroupResult
792 SHA256DigestGroupFailed
793 error
794 ordinal
795 internalIndex
796 before))))))))
797 groups)))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.