def bitw.first_set_is_set

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

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

470def bitw.first_set_is_set(+n: Nat, +w: Word(n), +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {A.bitw.test(n, w, k) == True{} : Bool}:
471  %bitw.index_some(A.bitw.ffs(n, w), k, e) : {bitw.at1(n, w, _) == nat.pos(_) : Bool}
472  bitw.ffs_set(n, w)