law first_set_lowest

bend-osdev-algo@0.1.0.0 · LAWS.bend:47

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

47law first_set_lowest:
48  for x: U32
49  for k: Nat
50  for j: Nat
51  for e: {A.bits32.first_set(x) == Some{k} : Maybe<&2, Nat>}
52  for l: {Nat.is_lt(j, k) == True{} : Bool}
53  {A.bits32.test(x, j) == False{} : Bool}

Uses (9)

Used by (0)

No other definition uses this definition.