AlphaGitHub
Source/Packages

Std.Word

packages/foundation/standard/src/Std/Word.alpha

1,783 lines192 declarations64.2 KiBSHA-256 27bf8c3f30ee
Download exact fileView at revision3c600751929f56cd01

def · lines 1763–1772

stdU32ShiftLeftChecked

Full file
CHECKED SHIFTS (U32): a count >= the width is an error; the wrapping `stdU32ShiftLeft/Right` (Model.Word32) repeat the one-bit shift `count` times, so a count >= 32 yields ZERO there (stated: NOT the x86-64 `shl` count-masking; a program wanting masking reduces the count itself).
1763def stdU32ShiftLeftChecked =
1764  (lambda unrestricted value : (family ModelWord32) .
1765    (lambda unrestricted count : Nat .
1766      (nat-eliminate
1767        (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
1768        (constructor StdOption StdNone (family ModelWord32))
1769        (lambda unrestricted predecessor : Nat .
1770          (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
1771            (constructor StdOption StdSome (family ModelWord32) (modelWord32ShiftLeft value count))))
1772        (nat-less-than count stdU32NaturalThirtyTwo))))

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.