PROOF.need_ok: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
Lines 43-48 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=43&end_line=48

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/validate.bend as V

def need_ok(b: Bool, -e: I.BpfError, h: {V.bpf_chk(b, e) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {b == True{} : Bool}:
  match b:
    case True{}:
      {==}
    case False{}:
      Empty.absurd({False{} == True{} : Bool}, absurd.fd(e, h))

Uses (7):
  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=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=absurd.fd
  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/validate.bend&name=bpf_chk