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 278–291

normalizationWordChoose

Full file
278def normalizationWordChoose =
279  (lambda unrestricted condition : Nat .
280    (lambda unrestricted selected : (pi unrestricted force : Nat . (family ModelWord32)) .
281      (lambda unrestricted fallback : (pi unrestricted force : Nat . (family ModelWord32)) .
282        (app
283          (nat-eliminate
284            (lambda unrestricted current : Nat .
285              (pi unrestricted force : Nat . (family ModelWord32)))
286            fallback
287            (lambda unrestricted predecessor : Nat .
288              (lambda unrestricted ignored : (pi unrestricted force : Nat . (family ModelWord32)) .
289                selected))
290            condition)
291          zero))))

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.