def dec_nil

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

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

574def dec_nil(r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> {dec.after(Nil{}, r) == r : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
575  match r:
576    case Fail{f}:
577      {==}
578    case Done{ops}:
579      {==}