def both_r

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

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

59def both_r(r: Result<&2, &2, I.BpfError, Unit>, -s: Result<&2, &2, I.BpfError, Unit>, h: {V.bpf_both(r, s) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}) -> {s == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
60  match r:
61    case Fail{e}:
62      Empty.absurd({s == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
63    case Done{u}:
64      h