1235def linuxAcceptBaseResponse =
1236 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
1237 (lambda unrestricted request : (family LinuxSyscallRequest) .
1238 (lambda unrestricted response : (family LinuxSyscallResponse) .
1239 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1240 (eliminate
1241 LinuxSyscallResponse
1242 (lambda unrestricted current : (family LinuxSyscallResponse) .
1243 (family LinuxSyscallReceiptDecision))
1244 response
1245 (branch
1246 LinuxOpenSucceeded
1247 descriptor
1248 .
1249 (linuxAcceptBaseSuccessfulKind
1250 request
1251 response
1252 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulOpenKind)
1253 audit))
1254 (branch
1255 LinuxReadSucceeded
1256 bytes
1257 .
1258 (linuxAcceptBaseSuccessfulKind
1259 request
1260 response
1261 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulReadKind)
1262 audit))
1263 (branch
1264 LinuxSeekSucceeded
1265 position
1266 .
1267 (linuxAcceptBaseSuccessfulKind
1268 request
1269 response
1270 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulSeekKind)
1271 audit))
1272 (branch
1273 LinuxWriteSucceeded
1274 written
1275 .
1276 (linuxAcceptBaseSuccessfulKind
1277 request
1278 response
1279 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulWriteKind)
1280 audit))
1281 (branch
1282 LinuxIoctlSucceeded
1283 output
1284 .
1285 (linuxAcceptBaseSuccessfulKind
1286 request
1287 response
1288 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulIoctlKind)
1289 audit))
1290 (branch
1291 LinuxMmapSucceeded
1292 address
1293 .
1294 (linuxAcceptBaseSuccessfulKind
1295 request
1296 response
1297 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulMmapKind)
1298 audit))
1299 (branch
1300 LinuxUnitSucceeded
1301 .
1302 (linuxAcceptBaseSuccessfulKind
1303 request
1304 response
1305 (constructor LinuxSuccessfulResponseKind LinuxSuccessfulUnitKind)
1306 audit))
1307 (branch
1308 LinuxSyscallFailed
1309 error
1310 errno
1311 .
1312 (nat-eliminate
1313 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1314 (constructor
1315 LinuxSyscallReceiptDecision
1316 LinuxSyscallReceiptFailed
1317 error
1318 errno
1319 audit)
1320 (lambda unrestricted interruptedPredecessor : Nat .
1321 (lambda unrestricted ignoredInterrupted : (family LinuxSyscallReceiptDecision) .
1322 (nat-eliminate
1323 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1324 (constructor
1325 LinuxSyscallReceiptDecision
1326 LinuxSyscallReceiptFailed
1327 error
1328 errno
1329 audit)
1330 (lambda unrestricted retryPredecessor : Nat .
1331 (lambda unrestricted ignoredRetry : (family LinuxSyscallReceiptDecision) .
1332 (constructor
1333 LinuxSyscallReceiptDecision
1334 LinuxSyscallReceiptRetryInterrupted
1335 invocation
1336 audit)))
1337 (linuxBaseRequestRetriesInterrupted request))))
1338 (linuxErrnoIsInterrupted errno))))))))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.