1500def linuxAcceptNativeSyscallReceipt =
1501 (lambda unrestricted invocation : (family LinuxNativeSyscallInvocation) .
1502 (lambda unrestricted receipt : (family LinuxNativeSyscallReceipt) .
1503 (nat-eliminate
1504 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1505 (linuxRejectReceipt
1506 (constructor LinuxSyscallContractErrorCode LinuxReceiptIdentityMismatch)
1507 (linuxReceiptAudit invocation receipt))
1508 (lambda unrestricted identityPredecessor : Nat .
1509 (lambda unrestricted ignoredIdentity : (family LinuxSyscallReceiptDecision) .
1510 (nat-eliminate
1511 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1512 (linuxAcceptIdentityMatchedReceipt invocation receipt)
1513 (lambda unrestricted fallbackPredecessor : Nat .
1514 (lambda unrestricted ignoredFallback : (family LinuxSyscallReceiptDecision) .
1515 (linuxRejectReceipt
1516 (constructor LinuxSyscallContractErrorCode LinuxReceiptHostFallbackRejected)
1517 (linuxReceiptAudit invocation receipt))))
1518 (linuxCleanupHostFallbackCount (linuxNativeReceiptTelemetry receipt)))))
1519 (linuxIdentityEqual
1520 (linuxNativeInvocationIdentity invocation)
1521 (linuxNativeReceiptIdentity receipt)))))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.