def bits.sub_zero

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

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

177def bits.sub_zero(+n: Nat, +x: Word(n)) -> {C.CapBits.subset(n, Word.zero(n), x) == True{} : Bool}:
178  match n:
179    case 0n:
180      {==}
181    case 1n+n1:
182      match x:
183        case WCon{True{}, +xt}:
184          bits.sub_zero(n1, xt)
185        case WCon{False{}, +xt}:
186          bits.sub_zero(n1, xt)