384def vaTakeObserved =
385 (lambda unrestricted eventIndex : Nat .
386 (lambda unrestricted size : ByteCount .
387 (lambda unrestricted allocator : (family VAAllocator) .
388 (eliminate
389 VAAllocator
390 (lambda unrestricted current : (family VAAllocator) . (family VAObservedResult))
391 allocator
392 (branch
393 VAAllocatorValue
394 inputNext
395 .
396 (app
397 (lambda unrestricted result : (family VAResult) .
398 (eliminate
399 VAResult
400 (lambda unrestricted current : (family VAResult) . (family VAObservedResult))
401 result
402 (branch
403 VASucceeded
404 allocation
405 .
406 (constructor
407 VAObservedResult
408 VAObservedResultValue
409 result
410 (vaTelemetrySucceededFor eventIndex inputNext size allocation)))
411 (branch
412 VAFailed
413 error
414 .
415 (constructor
416 VAObservedResult
417 VAObservedResultValue
418 result
419 (vaTelemetryFailed eventIndex inputNext size error)))))
420 (vaTake size allocator)))))))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.