AlphaGitHub
Source/Packages

Std.Word

packages/foundation/standard/src/Std/Word.alpha

1,783 lines192 declarations64.2 KiBSHA-256 27bf8c3f30ee
Download exact fileView at revisionf5034773ad4bb52133

def · lines 1363–1377

stdU32DivisionRun

Full file
1363def stdU32DivisionRun =
1364  (lambda unrestricted dividend : (family ModelWord32) .
1365    (lambda unrestricted divisor : (family ModelWord32) .
1366      (nat-eliminate
1367        (lambda unrestricted current : Nat . (family StdU32DivisionState))
1368        (constructor
1369          StdU32DivisionState
1370          StdU32DivisionStateOf
1371          modelWord32Zero
1372          modelWord32Zero
1373          dividend)
1374        (lambda unrestricted predecessor : Nat .
1375          (lambda unrestricted induction : (family StdU32DivisionState) .
1376            (stdU32DivisionStep divisor induction)))
1377        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.