package linksem

You can search for identifiers within the package.

in-package search v0.2.0

linksem_zarith

Legend:
Library
Module
Module type
Parameter
Class
Class type

val id0 : 'a -> 'a

val compare_byte : char -> char -> int

val instance_Basic_classes_Ord_Missing_pervasives_byte_dict : 
  char Lem_basic_classes.ord_class

val hex_char_of_nibble : Nat_big_num.num -> char

val hex_string_of_byte : char -> string

val instance_Show_Show_Missing_pervasives_byte_dict : char Show.show_class

val natural_of_decimal_digit : char -> Nat_big_num.num option

val natural_of_decimal_string_helper : 
  Nat_big_num.num ->
  char list ->
  Nat_big_num.num

val natural_of_decimal_string : string -> Nat_big_num.num

val hex_string_of_natural : Nat_big_num.num -> string

val natural_of_bool : bool -> Nat_big_num.num

val merge_by : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list

val mapMaybei' : 
  (Nat_big_num.num -> 'a -> 'b option) ->
  Nat_big_num.num ->
  'a list ->
  'b list

mapMaybei 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 mapMaybei : (Nat_big_num.num -> 'a -> 'b option) -> 'a list -> 'b list

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) list

partitionii 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 filteri : Nat_big_num.num list -> 'a list -> 'a list

val filterii : Nat_big_num.num list -> 'a list -> (Nat_big_num.num * 'a) list

val partitioni : Nat_big_num.num list -> 'a list -> 'a list * 'a list

val partitionii : 
  Nat_big_num.num list ->
  'a list ->
  (Nat_big_num.num * 'a) list * (Nat_big_num.num * 'a) list

val unzip3 : ('a * 'b * 'c) list -> 'a list * 'b list * 'c list

unzip3 ls takes a list of triples and returns a triple of lists.

val zip3 : 'a list -> 'b list -> 'c list -> ('a * 'b * 'c) list

zip3 ls takes a triple of lists and returns a list of triples.

null_byte is the null character a a byte.

val null_char : char

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.

val intercalate' : 'a -> 'a list -> 'a list -> 'a list

intercalate sep xs places sep between all elements of xs. * Made tail recursive and unrolled slightly to improve performance on large * lists.

val intercalate : 'a -> 'a list -> 'a list

val unlines : string list -> string

unlines xs concatenates a list of strings xs, placing each entry * on a new line.

val bracket : string list -> string

bracket xs concatenates a list of strings xs, separating each entry with a * space, and bracketing the resulting string.

val string_of_list : 'a Show.show_class -> 'a list -> string

string_of_list l produces a string representation of list l.

val instance_Show_Show_list_dict : 
  'a Show.show_class ->
  'a list Show.show_class

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.

val string_contains : string -> string -> bool

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.

val length : 'a list -> Nat_big_num.num

val takeRevAcc : Nat_big_num.num -> 'a list -> 'a list -> 'a list

val take0 : Nat_big_num.num -> 'a list -> 'a list

take cnt xs takes the first cnt elements of list xs. Returns a truncation * if cnt is greater than the length of xs.

val drop0 : Nat_big_num.num -> 'a list -> 'a list

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.

val string_index_of' : 
  'a ->
  'a list ->
  Nat_big_num.num ->
  Nat_big_num.num option

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.

val find_index_helper : 
  Nat_big_num.num ->
  ('a -> bool) ->
  'a list ->
  Nat_big_num.num option

val find_index0 : ('a -> bool) -> 'a list -> Nat_big_num.num option

val replicate_revacc : 'a list -> Nat_big_num.num -> 'a -> 'a list

val replicate0 : Nat_big_num.num -> 'a -> 'a list

val list_append : 'a list -> 'a list -> 'a list

val list_concat : 'a list list -> 'a list

val list_concat_map : ('a -> 'b list) -> 'a list -> 'b list

val list_reverse_concat_map_helper : 
  ('a -> 'b list) ->
  'b list ->
  'a list ->
  'b list

val list_reverse_concat_map : ('a -> 'b list) -> 'a list -> 'b list

val list_take_with_accum : Nat_num.nat -> 'a list -> 'a list -> 'a list

val unsafe_string_take : Nat_big_num.num -> string -> string

val padding_and_maybe_newline : char -> Nat_big_num.num -> string -> string

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.

val space_padding_and_maybe_newline : Nat_big_num.num -> string -> string

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.

val padded_and_maybe_newline : char -> Nat_big_num.num -> string -> string

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.

val padding_to : char -> Nat_big_num.num -> string -> string

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.

val left_padded_to : char -> Nat_big_num.num -> string -> string

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.

val right_padded_to : char -> Nat_big_num.num -> string -> string

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.

val space_padded_and_maybe_newline : Nat_big_num.num -> string -> string

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.

val left_space_padded_to : Nat_big_num.num -> string -> string

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.

val right_space_padded_to : Nat_big_num.num -> string -> string

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.

val left_zero_padded_to : Nat_big_num.num -> string -> string

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

val natural_of_char : char -> Nat_big_num.num

val natural_of_hex' : char list -> Nat_big_num.num

val natural_of_hex : string -> Nat_big_num.num

val assert_unwrap_maybe : 'a option -> 'a