171def nativeRegionContract =
172 (lambda unrestricted context : (family CheckpointEnvelopeContract) .
173 (lambda unrestricted schema : Bytes .
174 (lambda unrestricted extent : Nat .
175 (eliminate
176 CheckpointEnvelopeContract
177 (lambda unrestricted current : (family CheckpointEnvelopeContract) .
178 (family CheckpointEnvelopeContract))
179 context
180 (branch
181 CheckpointEnvelopeContractValue
182 original
183 learner
184 data
185 seed
186 payload
187 chunk
188 updates
189 .
190 (constructor
191 CheckpointEnvelopeContract
192 CheckpointEnvelopeContractValue
193 (bytes-builder-build
194 (bytes-builder-append
195 (checkpointManifestSized original)
196 (checkpointManifestSized schema)))
197 learner
198 data
199 seed
200 extent
201 extent
202 updates))))))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.