module Observe.Declaration

import Observe.Value
import Std.Natural

-- Compare distinct semantic variants while retaining each declaration's
-- origin. Unknown/truncated input never chooses the latest arrival as truth.
-- Codes: absent=0, agreed=1, conflicting=2, invalid=3, unsupported=4,
-- truncated=5. Negative transport counts are refused before interpretation.
def aosDeclarationAgreement =
  (lambda unrestricted variants : Nat . (lambda unrestricted invalid : Nat .
    (lambda unrestricted unsupported : Nat . (lambda unrestricted truncated : Nat .
      (aosChoose Nat (naturalNonzero truncated) 5
        (aosChoose Nat (naturalNonzero invalid) 3
          (aosChoose Nat (naturalNonzero unsupported) 4
            (aosChoose Nat (naturalEqual variants 0) 0
              (aosChoose Nat (naturalEqual variants 1) 1 2)))))))))