def tz
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as F64import Base
565# trailing zero bits of n (at most fuel)
566def tz(fuel: Nat, +n: Nat) -> Nat:
567 match fuel:
568 case 0n:
569 0n
570 case 1n+f:
571 pick(Nat, Nat.is_eq(Nat.mod(n, 2n), 1n), 0n, 1n+tz(f, Nat.div(n, 2n)))
Uses (5)
Used by (5)
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio:SMALL
- bend-collections-laws-math@1.0.0.0/spec/math/f64:as_ratio
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio:ctz_v
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio:cz
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64ratio:small_v