def both_l

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

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

50def both_l(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>}) -> {r == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}:
51  match r:
52    case Fail{e}:
53      Empty.absurd({Fail{e} == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}, absurd.fd(e, h))
54    case Done{u}:
55      match u:
56        case Unit{}:
57          {==}