AlphaGitHub
Source/Packages

Runtime.NativePhysicalProgramComposer

packages/execution/src/Runtime/NativePhysicalProgramComposer.alpha

1,548 lines120 declarations102.0 KiBSHA-256 d343a25865e7
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 253–268

nativePhysicalProgramComposeWord64FromNatural

Full file
253def nativePhysicalProgramComposeWord64FromNatural =
254  (lambda unrestricted value : Nat .
255    (nat-eliminate
256      (lambda unrestricted current : Nat . (family ModelWord64CheckedResult))
257      (constructor ModelWord64CheckedResult
258        ModelWord64CheckedSucceeded modelWord64Zero)
259      (lambda unrestricted predecessor : Nat .
260        (lambda unrestricted induction : (family ModelWord64CheckedResult) .
261          (eliminate ModelWord64CheckedResult
262            (lambda unrestricted current : (family ModelWord64CheckedResult) .
263              (family ModelWord64CheckedResult))
264            induction
265            (branch ModelWord64CheckedSucceeded prior .
266              (app (app modelWord64AddChecked prior) modelWord64One))
267            (branch ModelWord64CheckedFailed error . induction))))
268      value))

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.