AlphaGitHub
Source/Packages

Runtime.DeviceArenaCertificate

packages/execution/src/Runtime/DeviceArenaCertificate.alpha

1,800 lines133 declarations66.8 KiBSHA-256 74ef7fffbf20
Download exact fileView at revisionf5034773ad4bb52133

def · lines 351–359

deviceArenaSaturatingAdd

Full file
---- saturating words ----
351def deviceArenaSaturatingAdd =
352  (lambda unrestricted a : Nat .
353    (lambda unrestricted b : Nat .
354      (naturalAdd
355        a
356        (naturalSelect
357          (naturalLess (naturalSaturatingSubtract deviceArenaWordMaximum a) b)
358          (naturalSaturatingSubtract deviceArenaWordMaximum a)
359          b))))

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.