def CapBits.has

bend-osdev-caps@0.1.0.0 · caps.bend:228

import bend-osdev-caps@0.1.0.0/caps.bend as Caps
import Base

228# whether capability k is in s
229def CapBits.has(n: Nat, s: Word(n), k: Nat) -> Bool:
230  match n:
231    case 0n:
232      False{}
233    case 1n+p:
234      match s k:
235        case WCon{h, t} 0n:
236          h
237        case WCon{h, t} 1n+j:
238          CapBits.has(p, t, j)

Uses (4)

Used by (0)

No other definition uses this definition.