179def projectProtocolAnnouncements =
180 (lambda erased payload : Type 0 .
181 (lambda unrestricted role : Nat .
182 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
183 (eliminate
184 ProtocolAnnouncements
185 (lambda unrestricted current : (family ProtocolAnnouncements payload) .
186 (family ProtocolAnnouncements payload))
187 announcements
188 (branch
189 ProtocolAnnouncementsEnd
190 .
191 (constructor ProtocolAnnouncements ProtocolAnnouncementsEnd payload))
192 (branch
193 ProtocolAnnouncementsNext
194 identity
195 value
196 rest
197 induction
198 .
199 (nat-eliminate
200 (lambda unrestricted flag : Nat . (family ProtocolAnnouncements payload))
201 induction
202 (lambda unrestricted prior : Nat .
203 (lambda unrestricted ignored : (family ProtocolAnnouncements payload) .
204 (constructor
205 ProtocolAnnouncements
206 ProtocolAnnouncementsNext
207 payload
208 identity
209 value
210 induction)))
211 (naturalOr
212 (naturalEqual role (regionTransferSender identity))
213 (naturalEqual role (regionTransferReceiver identity)))))))))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.