PROOF.fin_done: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
Lines 1957-1962 of bend-osdev-bpf@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&start_line=1957&end_line=1962

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

def 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}:
  match r:
    case Fail{f}:
      Empty.absurd({Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run.fin(Fail{f})) == True{} : Bool}, absurd.ft(e))
    case Done{v}:
      {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result.is_done
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=absurd.ft
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompAction
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_run.fin