Process exit and exec refusal are different observations. Phase zero is an
exec refusal, phase one a completed wait. Flags are exact: invalid present
values (two) never count as absence (zero). Signals use signed exit values.
168def aosProgramEndAdmission =
169 (lambda unrestricted phase : Nat .
170 (lambda unrestricted exitCode : Nat .
171 (lambda unrestricted errorText : Nat .
172 (naturalOr
173 (naturalAnd
174 (naturalEqual phase 0)
175 (naturalAnd (naturalEqual exitCode 0) (naturalEqual errorText 1)))
176 (naturalAnd
177 (naturalEqual phase 1)
178 (naturalAnd (naturalEqual exitCode 1) (naturalEqual errorText 0)))))))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.