def bitw.fls_high

bend-osdev-algo@0.1.0.0 · PROOF.bend:331

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

331def bitw.fls_high(n: Nat, w: Word(n), j: Nat) -> {Bool.and(bitw.above(j, A.bitw.fls(n, w)), A.bitw.test(n, w, j)) == False{} : Bool}:
332  match n:
333    case 0n:
334      {==}
335    case 1n+ +p:
336      match w j:
337        case WCon{+b, t} 0n:
338          bitw.fls_high.z(A.bitw.fls(p, t), b)
339        case WCon{+b, +t} 1n+ +q:
340          bitw.fls_high.s(p, t, A.bitw.fls(p, t), b, q, bitw.fls_high(p, t, q))