def bitw.above

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

import Base

209# j lies above the highest set bit (every j does when there is none)
210def bitw.above(j: Nat, m: Nat) -> Bool:
211  match m:
212    case 0n:
213      True{}
214    case 1n+k:
215      Nat.is_lt(k, j)