338def vaTelemetrySucceededFor =
339 (lambda unrestricted eventIndex : Nat .
340 (lambda unrestricted inputNext : DeviceAddress .
341 (lambda unrestricted requestedBytes : ByteCount .
342 (lambda unrestricted allocation : (family VAAllocation) .
343 (eliminate
344 VAAllocation
345 (lambda unrestricted current : (family VAAllocation) . (family VATelemetry))
346 allocation
347 (branch
348 VAAllocationValue
349 start
350 extent
351 alignment
352 nextAllocator
353 .
354 (eliminate
355 VAAllocator
356 (lambda unrestricted current : (family VAAllocator) . (family VATelemetry))
357 nextAllocator
358 (branch
359 VAAllocatorValue
360 outputNext
361 .
362 (constructor
363 VATelemetry
364 VATelemetryValue
365 eventIndex
366 inputNext
367 requestedBytes
368 (constructor VAOptionalAlignment VASomeAlignment alignment)
369 start
370 extent
371 (stdByteCount
372 (modelWord64Subtract
373 (stdDeviceAddressValue start)
374 (stdDeviceAddressValue inputNext)))
375 (stdByteCount
376 (modelWord64Subtract
377 (stdByteCountValue extent)
378 (stdByteCountValue requestedBytes)))
379 outputNext
380 (succ zero)
381 (constructor VAOptionalError VANoError)
382 zero)))))))))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.