law wit_first_last

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

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

369# first_set and last_set answer Some (40 = 0b101000: bits 3 and 5), with a
370# j below and above; and None for zero
371law wit_first_last:
372  {(A.bits32.first_set(40), Nat.is_lt(1n, 3n), A.bits32.last_set(40), Nat.is_lt(5n, 7n), A.bits32.first_set(0), A.bits32.last_set(0)) == (Some{3n}, True{}, Some{5n}, True{}, None{}, None{}) : Maybe<&2, Nat> & Bool & Maybe<&2, Nat> & Bool & Maybe<&2, Nat> & Maybe<&2, Nat>}