Source/Packages

Observe.Metric

packages/observability/src/Observe/Metric.alpha

225 lines9 declarations10.4 KiBSHA-256 efa85c944576

def · lines 41–54

aosMetricAgreement

Full file
Missing source schemas are pending rather than guessed from another run. Existing invalid/unsupported/truncated input has precedence over pending.
41def aosMetricAgreement =
42  (lambda unrestricted variants : Nat .
43    (lambda unrestricted invalid : Nat .
44      (lambda unrestricted unsupported : Nat .
45        (lambda unrestricted truncated : Nat .
46          (lambda unrestricted pending : Nat .
47            (let unrestricted agreement =
48              (aosDeclarationAgreement variants invalid unsupported truncated)
49              in
50              (aosChoose
51                Nat
52                (naturalAnd (naturalNonzero pending) (naturalLessOrEqual agreement 2))
53                6
54                agreement)))))))

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.