def CapBits.single

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

import Base

216# the set holding capability k alone (empty if k >= n)
217def CapBits.single(n: Nat, k: Nat) -> Word(n):
218  match n:
219    case 0n:
220      WNil{}
221    case 1n+p:
222      match k:
223        case 0n:
224          WCon{True{}, Word.zero(p)}
225        case 1n+j:
226          WCon{False{}, CapBits.single(p, j)}