AlphaGitHub
Source/Packages

Runtime.TelemetryPublication

packages/execution/src/Runtime/TelemetryPublication.alpha

627 lines66 declarations23.6 KiBSHA-256 12de32412e73
Download exact fileView at revision426597bda5753d86c4

def · lines 535–555

publicationTypedEventCount

Full file
535def publicationTypedEventCount =
536  (lambda unrestricted records : (family StdList Bytes) .
537    (eliminate
538      StdList
539      (lambda unrestricted current : (family StdList Bytes) . Nat)
540      records
541      (branch StdListEmpty . 0)
542      (branch
543        StdListCons
544        head
545        tail
546        induction
547        .
548        (naturalAdd
549          induction
550          (eliminate
551            AosLine
552            (lambda unrestricted current : (family AosLine) . Nat)
553            (aosClassifyLine head)
554            (branch AosLineInvalid code . 0)
555            (branch AosLineValid record . (bytes-equal (aosMemberBytes b"type" record) b"event")))))))

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.