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 1637–1653

stdI32DivRemChecked

Full file
1637def stdI32DivRemChecked =
1638  (lambda unrestricted dividend : (family StdI32) .
1639    (lambda unrestricted divisor : (family StdI32) .
1640      (nat-eliminate
1641        (lambda unrestricted current : Nat . (family StdDivision (family StdI32)))
1642        (constructor
1643          StdDivision
1644          StdDivisionFailed
1645          (family StdI32)
1646          (constructor StdDivisionErrorCode StdDivisionOverflow))
1647        (lambda unrestricted predecessor : Nat .
1648          (lambda unrestricted induction : (family StdDivision (family StdI32)) .
1649            (stdI32DivRemWrapping dividend divisor)))
1650        (stdFlagNot
1651          (stdFlagAnd
1652            (stdU32Equal (stdI32ToWord dividend) stdI32MinimumBits)
1653            (stdU32Equal (stdI32ToWord divisor) stdU32AllOnes))))))

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.