AlphaGitHub
Source/Packages

Model.Word32Logic

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

142 lines9 declarations4.4 KiBSHA-256 ef93d5a70a2e
Download exact fileView at revisionf5034773ad4bb52133

def · lines 95–105

modelWord32RotateRight

Full file
95def modelWord32RotateRight =
96  (lambda unrestricted value : (family ModelWord32) .
97    (lambda unrestricted amount : Nat .
98      (app
99        (lambda unrestricted normalized : Nat .
100          (modelWord32Or
101            (modelWord32ShiftRight value normalized)
102            (modelWord32ShiftLeft
103              value
104              (naturalSaturatingSubtract modelWord32NaturalThirtyTwo normalized))))
105        (naturalModuloUnchecked amount modelWord32NaturalThirtyTwo))))

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.