AlphaGitHub
Source/Packages

Accelerator.SM86.FieldEncoding

packages/hardware/architectures/nvidia-sm86/src/Accelerator/SM86/FieldEncoding.alpha

861 lines86 declarations33.8 KiBSHA-256 1449867e9447
Download exact fileView at revisionf5034773ad4bb52133

def · lines 348–358

sm86FieldWord32InRange

Full file
348def sm86FieldWord32InRange : (pi unrestricted value : Nat . Nat) =
349  (lambda unrestricted value : Nat .
350    (nat-less-than
351      (naturalDivideUnchecked
352        (naturalDivideUnchecked
353          (naturalDivideUnchecked
354            (naturalDivideUnchecked value byteNaturalTwoHundredFiftySix)
355            byteNaturalTwoHundredFiftySix)
356          byteNaturalTwoHundredFiftySix)
357        byteNaturalTwoHundredFiftySix)
358      (succ 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.