AlphaGitHub
Source/Packages

Runtime.Protocol

packages/execution/src/Runtime/Protocol.alpha

531 lines78 declarations19.2 KiBSHA-256 8478a48f5a66
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 145–153

protocolAnnouncementsEmpty

Full file
145def protocolAnnouncementsEmpty =
146  (lambda erased payload : Type 0 .
147    (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
148      (eliminate
149        ProtocolAnnouncements
150        (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
151        announcements
152        (branch ProtocolAnnouncementsEnd . 1)
153        (branch ProtocolAnnouncementsNext identity value rest induction . 0))))

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.