~/jendhub

def caps.has_of

bend-osdev-caps@0.1.0.0 · PROOF.bend:709

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

709# a set that has capability k contains the set {k} (has is that subset test)
710def caps.has_of(+v: Bool, +s: C.CapSet(), +x: U32) -> {C.CapSet.has.go(v, s, x) == True{} : Bool} -> {C.CapSet.subset(C.CapSet.of.go(v, x), s) == True{} : Bool}:
711  match v:
712    case False{}:
713      h => bits.absurd(C.CapSet.subset(C.CapSet.of.go(False{}, x), s), h)
714    case True{}:
715      h => h

Uses (7)

Used by (1)