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 1571–1587

stdI64DivRemChecked

Full file
1571def stdI64DivRemChecked =
1572  (lambda unrestricted dividend : (family StdI64) .
1573    (lambda unrestricted divisor : (family StdI64) .
1574      (nat-eliminate
1575        (lambda unrestricted current : Nat . (family StdDivision (family StdI64)))
1576        (constructor
1577          StdDivision
1578          StdDivisionFailed
1579          (family StdI64)
1580          (constructor StdDivisionErrorCode StdDivisionOverflow))
1581        (lambda unrestricted predecessor : Nat .
1582          (lambda unrestricted induction : (family StdDivision (family StdI64)) .
1583            (stdI64DivRemWrapping dividend divisor)))
1584        (stdFlagNot
1585          (stdFlagAnd
1586            (modelWord64Equal (stdI64ToWord dividend) stdI64MinimumBits)
1587            (modelWord64Equal (stdI64ToWord divisor) stdU64AllOnes))))))

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.