AlphaGitHub
Source/Packages

Compiler.NormalizationBudget

packages/compiler/src/Compiler/NormalizationBudget.alpha

775 lines53 declarations32.9 KiBSHA-256 582a37dd050a
Download exact fileView at revisionf5034773ad4bb52133

def · lines 269–276

normalizationBytePredecessor

Full file
269def normalizationBytePredecessor =
270  (lambda unrestricted value : Byte .
271    (nat-to-byte
272      (nat-eliminate
273        (lambda unrestricted current : Nat . Nat)
274        (byte-to-nat (byte 255))
275        (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Nat . predecessor))
276        (byte-to-nat 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.