139def regionFrameHeader =
140 (lambda unrestricted identity : (family RegionTransferIdentity) .
141 (lambda unrestricted payloadBytes : Nat .
142 (lambda unrestricted headerBudget : Nat .
143 (eliminate
144 RegionTransferIdentity
145 (lambda unrestricted current : (family RegionTransferIdentity) .
146 (family StdResult (family RegionFrameFailure) Bytes))
147 identity
148 (branch
149 RegionTransferIdentityOf
150 composition
151 run
152 region
153 representation
154 round
155 operation
156 sender
157 receiver
158 interval
159 .
160 (eliminate
161 LearningRound
162 (lambda unrestricted current : (family LearningRound) .
163 (family StdResult (family RegionFrameFailure) Bytes))
164 round
165 (branch
166 LearningRoundOf
167 epoch
168 version
169 .
170 (regionFrameRequire
171 (naturalAnd
172 (naturalLessOrEqual headerBudget regionFrameWordLimit)
173 (naturalAnd
174 (naturalLessOrEqual payloadBytes regionFrameWordLimit)
175 (naturalAnd
176 (naturalLessOrEqual epoch regionFrameWordLimit)
177 (naturalAnd
178 (naturalLessOrEqual version regionFrameWordLimit)
179 (naturalAnd
180 (naturalLessOrEqual operation regionFrameWordLimit)
181 (naturalAnd
182 (naturalLessOrEqual sender regionFrameWordLimit)
183 (naturalAnd
184 (naturalLessOrEqual receiver regionFrameWordLimit)
185 (naturalAnd
186 (naturalLessOrEqual (intervalEnd interval) regionFrameWordLimit)
187 (naturalLessOrEqual
188 (intervalBegin interval)
189 (intervalEnd interval))))))))))
190 (constructor RegionFrameFailure RegionFrameBounds)
191 (lambda unrestricted delayed : Nat .
192 (regionFrameJoinWithin
193 (regionFrameChunk
194 regionFrameMagic
195 (regionFrameNumber
196 payloadBytes
197 (regionFrameName
198 composition
199 (regionFrameName
200 run
201 (regionFrameName
202 region
203 (regionFrameName
204 representation
205 (regionFrameNumber
206 epoch
207 (regionFrameNumber
208 version
209 (regionFrameChunk
210 (regionFrameRoute
211 operation
212 sender
213 receiver
214 (intervalBegin interval)
215 (intervalEnd interval))
216 (constructor StdList StdListEmpty Bytes))))))))))
217 headerBudget))))))))))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.