Counts and epochs enter word-valued runtime state only after admission.
The natural-to-binary64 conversion additionally needs the signed domain.
775def repeatedArtifactFor =
776 (lambda unrestricted endpoint : Nat .
777 (lambda unrestricted port : Nat .
778 (lambda unrestricted worker : Nat .
779 (lambda unrestricted weight : Nat .
780 (lambda unrestricted wrongMean : Nat .
781 (lambda unrestricted steps : Nat .
782 (lambda unrestricted epoch : Nat .
783 (lambda unrestricted version : Nat .
784 (nat-eliminate
785 (lambda unrestricted admitted : Nat . Bytes)
786 b""
787 (lambda unrestricted previous : Nat .
788 (lambda unrestricted ignored : Bytes .
789 (repeatedArtifactAdmitted
790 endpoint
791 port
792 worker
793 weight
794 wrongMean
795 steps
796 epoch
797 version)))
798 (naturalAnd
799 (naturalLessOrEqual steps regionFrameWordLimit)
800 (naturalAnd
801 (naturalLessOrEqual epoch regionFrameWordLimit)
802 (naturalAnd
803 (naturalLessOrEqual version regionFrameWordLimit)
804 (naturalLessOrEqual weight 9223372036854775807)))))))))))))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.