AlphaGitHub
Source/Packages

Runtime.NativePointwisePlan

packages/execution/src/Runtime/NativePointwisePlan.alpha

436 lines23 declarations18.6 KiBSHA-256 fd2fbc317365
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 133–144

nativePointwiseAdmitted

Full file
133def nativePointwiseAdmitted =
134  (lambda unrestricted slots : Nat .
135    (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
136      (lambda unrestricted base : Nat .
137        (lambda unrestricted available : Nat .
138          (naturalAnd
139            (nativePointwiseSupported slots program)
140            (naturalAnd
141              (naturalIsZero (naturalModuloUnchecked base nativePointwiseWordBytes))
142              (naturalAnd
143                (naturalLessOrEqual (nativePointwiseExtent slots program base) available)
144                (naturalBelowTwoPower 64 (nativePointwiseExtent slots program base)))))))))

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.