law wit_first_last64

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

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

374law wit_first_last64:
375  {(A.bits64.first_set(W.W64.from_parts(1, 0)), A.bits64.last_set(W.W64.from_parts(1, 0)), A.bits64.first_set(W.W64.zero())) == (Some{32n}, Some{32n}, None{}) : Maybe<&2, Nat> & Maybe<&2, Nat> & Maybe<&2, Nat>}