AlphaGitHub
Source/Packages

Observe.Stream

packages/observability/src/Observe/Stream.alpha

863 lines66 declarations29.5 KiBSHA-256 8d9909ce8db6
Download exact fileView at revision426597bda5753d86c4

def · lines 760–779

aosSumDrops

Full file
760def aosSumDrops =
761  (lambda unrestricted producers : (family StdList (family AosProducer)) .
762    (eliminate
763      StdList
764      (lambda unrestricted current : (family StdList (family AosProducer)) . Nat)
765      producers
766      (branch StdListEmpty . 0)
767      (branch
768        StdListCons
769        head
770        tail
771        induction
772        .
773        (naturalAdd
774          induction
775          (eliminate
776            AosProducer
777            (lambda unrestricted current : (family AosProducer) . Nat)
778            head
779            (branch AosProducerValue key next seen drops covered excluded mode . drops))))))

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.