AlphaGitHub
Source/Packages

Model.Word32

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

508 lines41 declarations18.3 KiBSHA-256 7f230128ec8c
Download exact fileView at revision426597bda5753d86c4

def · lines 300–313

modelWord32ShiftLeft

Full file
300def modelWord32ShiftLeft =
301  (lambda unrestricted value : (family ModelWord32) .
302    (lambda unrestricted amount : Nat .
303      (app
304        (nat-eliminate
305          (lambda unrestricted current : Nat . (pi unrestricted unit : Nat . (family ModelWord32)))
306          (lambda unrestricted unit : Nat . modelWord32Zero)
307          (lambda unrestricted predecessor : Nat .
308            (lambda unrestricted induction : (pi unrestricted unit : Nat . (family ModelWord32)) .
309              (lambda unrestricted unit : Nat .
310                (modelWord32FromNaturalTruncated
311                  (naturalMultiply (modelWord32ToNatural value) (naturalPowerOfTwo amount))))))
312          (naturalLess amount modelWord32NaturalThirtyTwo))
313        zero)))

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.