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 1698–1714

stdI16DivRemChecked

Full file
1698def stdI16DivRemChecked =
1699  (lambda unrestricted dividend : (family StdI16) .
1700    (lambda unrestricted divisor : (family StdI16) .
1701      (nat-eliminate
1702        (lambda unrestricted current : Nat . (family StdDivision (family StdI16)))
1703        (constructor
1704          StdDivision
1705          StdDivisionFailed
1706          (family StdI16)
1707          (constructor StdDivisionErrorCode StdDivisionOverflow))
1708        (lambda unrestricted predecessor : Nat .
1709          (lambda unrestricted induction : (family StdDivision (family StdI16)) .
1710            (stdI16DivRemWrapping dividend divisor)))
1711        (stdFlagNot
1712          (stdFlagAnd
1713            (stdU16Equal (stdI16ToU16 dividend) stdI16MinimumBits)
1714            (stdU16Equal (stdI16ToU16 divisor) stdU16AllOnes))))))

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.