The caller supplies a public scratch result slot for cleanup; private
recorder work slots are never exposed as application capabilities.
234def nativeObservedJournalClose =
235 (lambda unrestricted descriptorSlot : Nat .
236 (lambda unrestricted workSlot : Nat .
237 (lambda unrestricted error : Bytes .
238 (lambda unrestricted tail : (family NativePhysicalCommands) .
239 (nativeObservedJournalCall
240 3
241 (nativeLaunchRecipeArguments
242 (nativeLaunchRecipeSlotValue descriptorSlot)
243 (nativeLaunchRecipeImmediate 0)
244 (nativeLaunchRecipeImmediate 0)
245 (nativeLaunchRecipeImmediate 0))
246 b""
247 workSlot
248 error
249 (nativeLaunchRecipeAssertEqual
250 (nativeLaunchRecipeSlotValue workSlot)
251 (nativeLaunchRecipeImmediate 0)
252 error
253 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.