def absurd.fd

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

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

30def absurd.fd(-e: I.BpfError, h: {Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> Empty:
31  %h : absurd.res(_)
32  Unit{}