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 55–67

aosExecutionAdmission

Full file
Presentation metadata has no identity, authorization or execution-outcome authority. Only a declaration bound to its source run with every admitted field may contribute a name. Unknown validation flags fail closed.
55def aosExecutionAdmission =
56  (lambda unrestricted identity : Nat .
57    (lambda unrestricted namespace : Nat .
58      (lambda unrestricted name : Nat .
59        (lambda unrestricted kind : Nat .
60          (lambda unrestricted origin : Nat .
61            (naturalAnd
62              (naturalEqual identity 1)
63              (naturalAnd
64                (naturalEqual namespace 1)
65                (naturalAnd
66                  (naturalEqual name 1)
67                  (naturalAnd (naturalEqual kind 1) (naturalEqual origin 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.