157def modelWord32ShiftRightOne =
158 (lambda unrestricted value : (family ModelWord32) .
159 (eliminate
160 ModelWord32
161 (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
162 value
163 (branch
164 ModelWord32Value
165 b0
166 b1
167 b2
168 b3
169 .
170 (constructor
171 ModelWord32
172 ModelWord32Value
173 (byteOr
174 (byteShiftRight b0 modelWord32NaturalOne)
175 (byteShiftLeftTruncated (byteAnd b1 (byte 1)) modelWord32NaturalSeven))
176 (byteOr
177 (byteShiftRight b1 modelWord32NaturalOne)
178 (byteShiftLeftTruncated (byteAnd b2 (byte 1)) modelWord32NaturalSeven))
179 (byteOr
180 (byteShiftRight b2 modelWord32NaturalOne)
181 (byteShiftLeftTruncated (byteAnd b3 (byte 1)) modelWord32NaturalSeven))
182 (byteShiftRight b3 modelWord32NaturalOne)))))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.