def fin_done

bend-osdev-bpf@0.1.0.0 · PROOF.bend:1957

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/seccomp.bend as S

1957def fin_done(r: Result<&2, &2, I.BpfError, U32>, e: {Result.is_done(&2, &2, I.BpfError, U32, r) == True{} : Bool}) -> {Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run.fin(r)) == True{} : Bool}:
1958  match r:
1959    case Fail{f}:
1960      Empty.absurd({Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run.fin(Fail{f})) == True{} : Bool}, absurd.ft(e))
1961    case Done{v}:
1962      {==}