AlphaGitHub
Source/Packages

Model.Word32

packages/foundation/standard/src/Model/Word32.alpha

492 lines41 declarations17.0 KiBSHA-256 eb985612415b
Download exact fileView at revisionf5034773ad4bb52133

def · lines 184–209

modelWord32ShiftLeftOne

Full file
184def modelWord32ShiftLeftOne =
185  (lambda unrestricted value : (family ModelWord32) .
186    (eliminate
187      ModelWord32
188      (lambda unrestricted current : (family ModelWord32) . (family ModelWord32))
189      value
190      (branch
191        ModelWord32Value
192        b0
193        b1
194        b2
195        b3
196        .
197        (constructor
198          ModelWord32
199          ModelWord32Value
200          (byteShiftLeftTruncated b0 modelWord32NaturalOne)
201          (byteOr
202            (byteShiftLeftTruncated b1 modelWord32NaturalOne)
203            (byteShiftRight b0 modelWord32NaturalSeven))
204          (byteOr
205            (byteShiftLeftTruncated b2 modelWord32NaturalOne)
206            (byteShiftRight b1 modelWord32NaturalSeven))
207          (byteOr
208            (byteShiftLeftTruncated b3 modelWord32NaturalOne)
209            (byteShiftRight b2 modelWord32NaturalSeven))))))

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.