package linksem
Install
Dune Dependency
Authors
Maintainers
Sources
md5=2075c56715539b3b8f54ae65cc808b8c
sha512=f7c16e4036a1440a6a8d13707a43f0f9f9db0c68489215f948cc300b6a164dba5bf852e58f89503e9d9f38180ee658d9478156ca1a1ef64d6861eec5f9cf43d2
doc/linksem_zarith/Missing_pervasives/index.html
Module Missing_pervasivesSource
val instance_Basic_classes_Ord_Missing_pervasives_byte_dict :
char Lem_basic_classes.ord_classval mapMaybei' :
(Nat_big_num.num -> 'a -> 'b option) ->
Nat_big_num.num ->
'a list ->
'b listmapMaybei f xs maps a function expecting an index (the position in the list * xs that it is currently viewing) and producing a maybe type across a list. * Elements that produce Nothing under f are discarded in the output, whilst * those producing Just e for some e are kept.
val partitionii' :
Nat_big_num.num ->
Nat_big_num.num list ->
'a list ->
(Nat_big_num.num * 'a) list ->
(Nat_big_num.num * 'a) list ->
(Nat_big_num.num * 'a) list * (Nat_big_num.num * 'a) listpartitionii is xs returns a pair of lists: firstly those elements in xs that are at indices in is, and secondly the remaining elements. It preserves the order of elements in xs.
val partitionii :
Nat_big_num.num list ->
'a list ->
(Nat_big_num.num * 'a) list * (Nat_big_num.num * 'a) listunzip3 ls takes a list of triples and returns a triple of lists.
zip3 ls takes a triple of lists and returns a list of triples.
null_byte is the null character a a byte.
null_char is the null character.
println s prints s to stdout, adding a trailing newline.
prints s prints s to stdout, without adding a trailing newline.
errln s prints s to stderr, adding a trailing newline.
errs s prints s to stderr, without adding a trailing newline.
outln s prints s to stdout, adding a trailing newline.
outs s prints s to stdout, without adding a trailing newline.
intercalate sep xs places sep between all elements of xs. * Made tail recursive and unrolled slightly to improve performance on large * lists.
unlines xs concatenates a list of strings xs, placing each entry * on a new line.
bracket xs concatenates a list of strings xs, separating each entry with a * space, and bracketing the resulting string.
string_of_list l produces a string representation of list l.
split_string_on_char s c splits a string s into a list of substrings * on character c, otherwise returning the singleton list containing s * if c is not found in s. * * NOTE: quirkily, this doesn't discard separators (e.g. because NUL characters * are significant when indexing into string tables). FIXME: given this, is this * function really reusable? I suspect not.
string_of_nat m produces a string representation of natural number m.
string_suffix i s returns all but the first i characters of s. * Fails if the index is negative, or beyond the end of the string.
take cnt xs takes the first cnt elements of list xs. Returns a truncation * if cnt is greater than the length of xs.
drop cnt xs returns all but the first cnt elements of list xs. Returns an empty list * if cnt is greater than the length of xs.
string_prefix i s returns the first i characters of s. * Fails if the index is negative, or beyond the end of the string.
string_index_of c s returns Just(i) where i is the index of the first * occurrence if c in s, if it exists, otherwise returns Nothing.
padding_and_maybe_newline c w s creates enough of char c to pad string s to w characters, * unless s is of length w - 1 or greater, in which case it generates w copies preceded by a newline. * This style of formatting is used by the GNU linker in its link map output, so we * reproduce it using this function. Note that string s does not appear in the * output.
space_padding_and_maybe_newline w s creates enoughspaces to pad string s to w characters, * unless s is of length w - 1 or greater, in which case it generates w copies preceded by a newline. * This style of formatting is used by the GNU linker in its link map output, so we * reproduce it using this function. Note that string s does not appear in the * output.
padded_and_maybe_newline w s pads string s to w characters, using char c * unless s is of length w - 1 or greater, in which case the padding consists of * w copies of c preceded by a newline. * This style of formatting is used by the GNU linker in its link map output, so we * reproduce it using this function.
padding_to c w s creates enough copies of c to pad string s to w characters, * or 0 characters if s is of length w or greater. Note that string s does not appear in the * output.
left_padded_to c w s left-pads string s to w characters using c, * returning it unchanged if s is of length w or greater.
right_padded_to c w s right-pads string s to w characters using c, * returning it unchanged if s is of length w or greater.
space_padded_and_maybe_newline w s pads string s to w characters, using spaces, * unless s is of length w - 1 or greater, in which case the padding consists of * w spaces preceded by a newline. * This style of formatting is used by the GNU linker in its link map output, so we * reproduce it using this function.
left_space_padded_to w s left-pads string s to w characters using spaces, * returning it unchanged if s is of length w or greater.
right_space_padded_to w s right-pads string s to w characters using spaces, * returning it unchanged if s is of length w or greater.
left_zero_padded_to w s left-pads string s to w characters using zeroes, * returning it unchanged if s is of length w or greater.
hex parsing