AlphaGitHub
Source/Packages

Observe.Execution

packages/observability/src/Observe/Execution.alpha

178 lines7 declarations7.2 KiBSHA-256 8a1b0821a355
Download exact fileView at revision426597bda5753d86c4

def · lines 40–50

aosProgramOutputSelectionAdmission

Full file
Explicit local output selections require a recorder and bounded valid paths. Selecting a file associates it with a launch; it does not prove who wrote it.
40def aosProgramOutputSelectionAdmission =
41  (lambda unrestricted count : Nat .
42    (lambda unrestricted recorder : Nat .
43      (lambda unrestricted paths : Nat .
44        (naturalAnd
45          (naturalLessOrEqual count 64)
46          (naturalAnd
47            (naturalEqual paths 1)
48            (naturalAnd
49              (naturalLessOrEqual recorder 1)
50              (naturalOr (naturalEqual count 0) (naturalEqual recorder 1))))))))

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.