def bitw.fls_high.z

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

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

309def bitw.fls_high.z(m: Nat, b: Bool) -> {Bool.and(bitw.above(0n, A.bitw.fls.step(m, b)), b) == False{} : Bool}:
310  match m:
311    case 0n:
312      match b:
313        case True{}:
314          {==}
315        case False{}:
316          {==}
317    case 1n+k:
318      {==}