1218def linuxAcceptBaseSuccessfulKind =
1219 (lambda unrestricted request : (family LinuxSyscallRequest) .
1220 (lambda unrestricted response : (family LinuxSyscallResponse) .
1221 (lambda unrestricted observed : (family LinuxSuccessfulResponseKind) .
1222 (lambda unrestricted audit : (family LinuxSyscallReceiptAudit) .
1223 (nat-eliminate
1224 (lambda unrestricted current : Nat . (family LinuxSyscallReceiptDecision))
1225 (linuxRejectReceipt
1226 (constructor LinuxSyscallContractErrorCode LinuxReceiptResponseKindMismatch)
1227 audit)
1228 (lambda unrestricted predecessor : Nat .
1229 (lambda unrestricted induction : (family LinuxSyscallReceiptDecision) .
1230 (linuxAcceptBaseSuccess response audit)))
1231 (naturalEqual
1232 (linuxSuccessfulResponseKindRank (linuxExpectedSuccessfulResponseKind request))
1233 (linuxSuccessfulResponseKindRank observed)))))))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.