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 1741–1757

stdI8DivRemChecked

Full file
1741def stdI8DivRemChecked =
1742  (lambda unrestricted dividend : (family StdI8) .
1743    (lambda unrestricted divisor : (family StdI8) .
1744      (nat-eliminate
1745        (lambda unrestricted current : Nat . (family StdDivision (family StdI8)))
1746        (constructor
1747          StdDivision
1748          StdDivisionFailed
1749          (family StdI8)
1750          (constructor StdDivisionErrorCode StdDivisionOverflow))
1751        (lambda unrestricted predecessor : Nat .
1752          (lambda unrestricted induction : (family StdDivision (family StdI8)) .
1753            (stdI8DivRemWrapping dividend divisor)))
1754        (stdFlagNot
1755          (stdFlagAnd
1756            (byte-equal (stdI8ToByte dividend) (byte 128))
1757            (byte-equal (stdI8ToByte divisor) (byte 255)))))))

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.