PROOF.ex.result: def of bend-osdev-caps@0.1.0.0
Import: import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF
Lines 805-810 of bend-osdev-caps@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-caps@0.1.0.0/PROOF.bend&start_line=805&end_line=810

import Base
import bend-osdev-caps@0.1.0.0/caps.bend as C
import bend-osdev-caps@0.1.0.0/exec.bend as E

def ex.result(+ok: Bool, +c: C.CapCred, +eu: U32, +s: C.CapState) -> {C.Caps.sets_or(E.CapExec.fin(ok, c, eu, s), s) == s : C.CapState}:
  match ok c:
    case False{} c:
      {==}
    case True{} C.CapCred{r, e, sv, nr, na, st}:
      {==}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapCred
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=CapState
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/caps.bend&name=Caps.sets_or
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-caps@0.1.0.0/exec.bend&name=CapExec.fin