law first_set64_none

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

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

125law first_set64_none:
126  for a: W.W64
127  for e: {A.bits64.first_set(a) == None{} : Maybe<&2, Nat>}
128  {a == W.W64.zero() : W.W64}