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

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

def dec_step(m: Maybe<&2, I.BpfOp>, -e: I.BpfError, -acc: List<&2, I.BpfOp>, r: Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>) -> {dec.after2(I.bpf_decode.push(m, e, acc), r) == dec.after(acc, I.bpf_decode.cons(m, e, r)) : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
  match m:
    case None{}:
      {==}
    case Some{op}:
      match r:
        case Fail{f}:
          {==}
        case Done{ops}:
          {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=dec.after
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=dec.after2
  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/insn.bend&name=BpfOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_decode.cons
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_decode.push