Index of values

abs_compl s is the absolute complement ∁ s.

add p s is the union s ∪ of_prefix p.

appose sA sB is the set whose lower and upper halves are sA and sB shrunk to half their size by prefixing their elements by 0 and 1, respectively.

bitnot s is the string s' such that get i s = not (get i s').

The constant const 1 false.

The constant const 1 true.

cat s0 s1 is the concatenation of s0 and s1.

compare sA sB returns -1, 0, or 1 when sA is less, equal, or greater than sB, respectively, according to lexicographical ordering of bits.

compl_decomp s returns a pair (sC, sA) such that s equals sA ∖ sC.

const n x is the n-bit string of x.

coprefix_length sA sB is the largest n such that get i sA = get i sB for i < n.

coslice_length iA sA iB sB is the largest n such that get (iA + i) sA = get (iB + i) sB for i < n.

cover_card s is the cardinality of the minimal set of prefixes which cover of s.

cover_find p s returns the cover of p in s or raises Not_found is no such cover exist in s.

disjoint sA sB is true iff sA ∩ sB is the empty set.

The empty set.

The empty bit-string.

equal sA sB is true iff sA and sB contain the same members.

equal sA sB is true iff sA and sB are bitwise equal.

fold f s is the function f p_(n-1) ∘ ⋯ ∘ f p_0 where {p_i} is the minimal set of prefixes which cover s.

Given a string s of length n, fold f s returns f (get (n - 1) s) ∘ ⋯ ∘ f (get 0 s).

Given a string s of length n, foldi f s is the function f (n - 1) (get (n - 1) s) ∘ ⋯ ∘ f 0 (get 0 s).

Given a string s of length n, foldi16 f s is the function f (⌈n/16⌉ - 1) (get (⌈n/16⌉ - 1) s) ∘ ⋯ ∘ f 0 (get 0 s).

Given a string s of length n, foldi8 f s is the function f (⌈n/8⌉ - 1) (get (⌈n/8⌉ - 1) s) ∘ ⋯ ∘ f 0 (get 0 s).

get i s is true iff the ith bit of s is set.

get16 i s is the integer with bit number 15 - j equal to bit number 16*i + j of s.

get8 i s is the integer with bit number 7 - j equal to bit number 8*i + j of s.

has_prefix s0 s is true iff s starts with s0.

has_slice s0 i s is true iff s contains a substring equal to s0 starting at bit number i.

has_suffix s0 s is true iff s ends with s0.

init n f turns the predicate f into a bit-string s of length n such that f i = get f i for 0 ≤ i < n.

init16 n f is the n-bit string s such that get (16*i + j) s is true iff bit number 15 - j of f i is set.

init8 n f is the n-bit string s such that get (8*i + j) s is true iff bit number 7 - j of f i is set.

intersect p s is the intersection s ∩ of_prefix p.

True on the empty set, false elsewhere.

True on the empty path, elsewhere false.

True for sets s such that equal s (of_prefix p) for some p.

is_universe s is true iff equal s universe.

isecn sA sB is the intersection sA ∩ sB.

iter f s calls f for each prefix in the minimal cover for s.

iter f s calls f on each element of s in order.

iteri f s calls f i (get i s) for 0 ≤ i < length s in order.

length s is the number of bits contained in s.

length16 s = ⌈length s / 16⌉.

length8 s = ⌈length s / 8⌉.

lower_half s is the set {p | 0·p ∈ s}.

Given s of length n, then map f s is the n-bit string s' such that get i s' = f (get i s) for 0 ≤ i < n.

Given s of length n, then mapi f s is the n-bit string s' such that get i s' = f i (get i s) for 0 ≤ i < n.

modify f p s is the set s ∖ of_prefix p ∪ unzoom (f (zoom s)).

of_array16 xa forms a bitpath by composing hexadecatets of xa, staring with the most significant.

of_array8 xa forms a bitpath by composing the octets from xa, starting with the most significant.

of_bin_string ~n s8 converts an octet string s8 to a bit string s1, where get (8*i + j) s1 equals bit number 7 - j of String.get i s8.

of_hex_string ~n str returns the bitstring described by the hexadecimal string str, clipped to n bits if specified.

of_prefix p is the set of all strings starting with p.

of_string s interprets a string s of '0' and '1' characters as a bit string.

pick_first s returns the lexicographically lowest prefix describing a cover in s.

pick_random s returns a random prefix of s, using the PRNG from the Random module.

prefix i s is the substring containing the i first bits of s.

rel_compl sC sA is the relative complement sA ∖ sC.

remove p s is the relative complement s ∖ of_prefix p.

slice i j s is the sub-string of bit i to j - 1 of s.

suffix i s is the substring containing all but the i first bits of s.

to_bin_string ~n s converts a bit string to an octet string using the same representation as of_bit_string.

to_hex_string ~n s is the hexadecimal encoding of s padded with zeros to the next quartet, or clipped or padded to n bits if specified.

If is_prefix s, then to_prefix s returns the p such that equal s (of_prefix p), otherwise it raises Invalid_argument.

to_string s turns s to a textual representation of '0' and '1' characters, starting with the lowest index.

union sA sB is the union sA ∪ sB.

The set containing all infinite bit-strings.

unzoom p s is the set {p·p' | p' ∈ s}.

upper_half s is the set {p | 1·p ∈ s}.

zoom p s is the set {p' | p·p' ∈ s}.