712def modelWord64FromNaturalTruncated =
713 (lambda unrestricted value : Nat .
714 (app
715 (lambda unrestricted quotient1 : Nat .
716 (app
717 (lambda unrestricted quotient2 : Nat .
718 (app
719 (lambda unrestricted quotient3 : Nat .
720 (app
721 (lambda unrestricted quotient4 : Nat .
722 (app
723 (lambda unrestricted quotient5 : Nat .
724 (app
725 (lambda unrestricted quotient6 : Nat .
726 (app
727 (lambda unrestricted quotient7 : Nat .
728 (constructor
729 ModelWord64
730 ModelWord64Value
731 (nat-to-byte
732 (naturalModuloUnchecked value byteNaturalTwoHundredFiftySix))
733 (nat-to-byte
734 (naturalModuloUnchecked quotient1 byteNaturalTwoHundredFiftySix))
735 (nat-to-byte
736 (naturalModuloUnchecked quotient2 byteNaturalTwoHundredFiftySix))
737 (nat-to-byte
738 (naturalModuloUnchecked quotient3 byteNaturalTwoHundredFiftySix))
739 (nat-to-byte
740 (naturalModuloUnchecked quotient4 byteNaturalTwoHundredFiftySix))
741 (nat-to-byte
742 (naturalModuloUnchecked quotient5 byteNaturalTwoHundredFiftySix))
743 (nat-to-byte
744 (naturalModuloUnchecked quotient6 byteNaturalTwoHundredFiftySix))
745 (nat-to-byte
746 (naturalModuloUnchecked quotient7 byteNaturalTwoHundredFiftySix))))
747 (naturalDivideUnchecked quotient6 byteNaturalTwoHundredFiftySix)))
748 (naturalDivideUnchecked quotient5 byteNaturalTwoHundredFiftySix)))
749 (naturalDivideUnchecked quotient4 byteNaturalTwoHundredFiftySix)))
750 (naturalDivideUnchecked quotient3 byteNaturalTwoHundredFiftySix)))
751 (naturalDivideUnchecked quotient2 byteNaturalTwoHundredFiftySix)))
752 (naturalDivideUnchecked quotient1 byteNaturalTwoHundredFiftySix)))
753 (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)))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.