One-based argument insertion for an explicitly requested native assignment.
The launcher must have a recorder, and may append one position after the
supplied arguments. Bounds are checked before compiling or creating a file.
26def aosProgramAssignmentArgumentAdmission =
27 (lambda unrestricted argument : Nat .
28 (lambda unrestricted supplied : Nat .
29 (lambda unrestricted recorder : Nat .
30 (naturalAnd
31 (naturalEqual recorder 1)
32 (naturalAnd
33 (naturalLess 0 argument)
34 (naturalAnd
35 (naturalLessOrEqual argument 4096)
36 (naturalLessOrEqual argument (succ supplied))))))))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.