def F_decode
bend-osdev-bpf@0.1.0.0 · PROOF.bend:581
import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
581def F_decode(+rs: List<&2, I.BpfRaw>) -> {I.bpf_decode.ref(rs) == I.bpf_decode(rs) : Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>}:
582 Equal.sym(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode(rs), I.bpf_decode.ref(rs),
583 Equal.trans(Result<&2, &2, I.BpfError, List<&2, I.BpfOp>>, I.bpf_decode(rs), dec.after(Nil{}, I.bpf_decode.ref.go(rs, 0n)), I.bpf_decode.ref.go(rs, 0n),
584 g_decode(rs, 0n, Done{Nil{}}), dec_nil(I.bpf_decode.ref.go(rs, 0n))))