proofs/containers/bitset/model.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/bitset/model.bend as Model
2 imports
import Base import ../../../src/containers/bitset.bend as B
Definitions
def zeros source · line 20 · raw
@n:Nat -> @free:Nat -> List<&2, U32>
Zero words covering n more bits; free counts unused bits left in the
last emitted word, so exactly ceil(n/32) words are produced from free = 0.
def get_pick source · line 29 · raw
@b:Bool -> @w:U32 -> @+i:Nat -> @r:Bool -> Bool
def get_walk source · line 36 · raw
@ws:List<&2, U32> -> @+i:Nat -> Bool
def put_pick source · line 43 · raw
@b:Bool -> @+v:Bool -> @+w:U32 -> @+i:Nat -> @t:List<&2, U32> -> @r:List<&2, U32> -> List<&2, U32>
def put_walk source · line 50 · raw
@+ws:List<&2, U32> -> @+i:Nat -> @+v:Bool -> List<&2, U32>
def zip_words source · line 57 · raw
@+k:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/bitset.WordOp -> @ws:List<&2, U32> -> @vs:List<&2, U32> -> List<&2, U32>
def count_words source · line 64 · raw
@ws:List<&2, U32> -> Nat
def members_words source · line 71 · raw
@ws:List<&2, U32> -> @+off:Nat -> List<&2, Nat>