The raw command fold above is internal to these two admission entries.
403def nativePointwiseProgram =
404 (lambda unrestricted slots : Nat .
405 (lambda unrestricted program : (family StdList (family PointwiseAssignment StdU64 slots)) .
406 (lambda unrestricted base : Nat .
407 (lambda unrestricted available : Nat .
408 (lambda unrestricted scratch : Nat .
409 (lambda erased admitted : (equal Nat (nativePointwiseAdmitted slots program base available) 1) .
410 (nativePointwiseCommands slots program base available scratch)))))))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.