def bitw.below

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

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF

import Base

201# j lies below the lowest set bit (every j does when there is none)
202def bitw.below(j: Nat, m: Nat) -> Bool:
203  match m:
204    case 0n:
205      True{}
206    case 1n+k:
207      Nat.is_lt(j, k)

Uses (3)

Used by (4)