544def bobWriteAt =
545 (lambda unrestricted file : (family NvidiaPlanHostFile) .
546 (lambda unrestricted address : Nat .
547 (lambda unrestricted extent : Nat .
548 (lambda unrestricted offset : Nat .
549 (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
550 (constructor
551 NvidiaPlanHostSteps
552 NvidiaPlanHostStepWriteAt
553 file
554 (bobStagingAt address)
555 extent
556 offset
557 tail))))))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.