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 1774–1783

stdU32ShiftRightChecked

Full file
1774def stdU32ShiftRightChecked =
1775  (lambda unrestricted value : (family ModelWord32) .
1776    (lambda unrestricted count : Nat .
1777      (nat-eliminate
1778        (lambda unrestricted current : Nat . (family StdOption (family ModelWord32)))
1779        (constructor StdOption StdNone (family ModelWord32))
1780        (lambda unrestricted predecessor : Nat .
1781          (lambda unrestricted induction : (family StdOption (family ModelWord32)) .
1782            (constructor StdOption StdSome (family ModelWord32) (modelWord32ShiftRight value count))))
1783        (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.