1180def linuxAcceptBaseSuccess =
1181 (lambda unrestricted response : (family LinuxSyscallResponse) .
1182 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1183 (nat-eliminate
1184 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1185 (constructor LinuxSyscallReceiptDecision LinuxSyscallReceiptAcceptedBase response audit)
1186 (lambda unrestricted predecessor : Nat .
1187 (lambda unrestricted induction : (family LinuxSyscallReceiptDecision) .
1188 (linuxRejectReceipt
1189 (constructor LinuxSyscallContractErrorCode LinuxReceiptCleanupFailed)
1190 audit)))
1191 (linuxCleanupFailureCount
1192 (eliminate
1193 LinuxSyscallReceiptAudit
1194 (lambda unrestricted current : (family LinuxSyscallReceiptAudit) .
1195 (family LinuxSyscallReceiptTelemetry))
1196 audit
1197 (branch LinuxSyscallReceiptAuditValue expected actual telemetry . telemetry))))))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.