Module functions

Source

Expand description

Auto-generated module

🤖 Generated with SplitRS

Functions§

apply_substitutions: Apply a substitution map to a string, replacing all occurrences of each key with its value.
box_title: Box-draw a title line.
build_line_starts: Build a table mapping line numbers (0-indexed) to their byte start positions.
build_string_env: Build the standard String environment declarations.
byte_pos_to_line_col: Convert a BytePos to a LineCol within a source string.
camel_to_snake: Convert a camelCase or PascalCase string to snake_case.
capitalize: Capitalize the first character of a string.
center: Center s within width characters, padding with spaces.
char_count: Count the number of Unicode code points in a string.
chunk_chars: Split a string into fixed-size chunks of n characters.
closest_match: Find the closest match from candidates to query by Levenshtein distance.
components_to_dotted_name: Convert a list of components back to a dotted name string.
count_occurrences: Count non-overlapping occurrences of needle in haystack.
decapitalize: Lowercase the first character of a string.
deduplicate_consecutive: Remove duplicate consecutive characters from a string.
dotted_name_last: Return the last component of a dotted name.
dotted_name_namespace: Return the namespace prefix of a dotted name (everything before the last .).
dotted_name_to_components: Convert a dotted name string ("Foo.bar.Baz") to a path of components.
edit_distance: Compute the Levenshtein edit distance between two strings.
escape_for_display: Escape a string for display in error messages or pretty-printed output.
format_list: Format a list of items with a separator.
format_opt: Format an optional value, using default if absent.
format_paren_list: Format a list of items in parentheses, comma-separated.
glob_helper
glob_match: Check whether a string matches a glob pattern (supports * and ?).
hr: Create a horizontal rule of n dashes.
in_namespace: Check whether a name is in a given namespace.
indent: Indent every line of text by n spaces.
indent_continuation: Add n spaces of indent to the first line and continuation_indent to the rest.
interleave_char: Insert a separator between characters in a string.
is_all_alpha: Return true if s contains only ASCII letters.
is_all_digits: Return true if s contains only ASCII digits.
is_blank: Check whether s contains only ASCII whitespace.
is_palindrome: Check whether a string is a palindrome.
is_valid_ident: Check whether s is a valid OxiLean/Lean 4 identifier.
join: Join parts with sep between them.
lean4_check: Format a Lean 4 #check command string.
lean4_def_stub: Format a Lean 4 def stub.
lean4_quote_ident: Surround s with backticks for Lean 4 identifier quoting.
lean4_theorem_stub: Format a Lean 4 theorem declaration stub.
mangle_name: Mangle an OxiLean name to a C/LLVM-safe identifier.
normalize_whitespace: Normalise all runs of whitespace in text to a single space.
nth_char: Return the nth Unicode code point (0-indexed), or None if out of range.
pad_left: Pad s on the left with spaces to reach at least width chars.
pad_right: Pad s on the right with spaces to reach at least width chars.
register_string_extended_axioms: Register all extended string axioms in the environment.
repeat_str: Repeat s exactly n times.
replace_first: Replace the first occurrence of from in s with to.
reverse_str: Reverse a string by Unicode code points.
sentence_count: Count sentences (splits on ., !, ?).
slugify: Slugify a string: lowercase, replace spaces and punctuation with -.
snake_to_camel: Convert a snake_case string to camelCase.
snake_to_pascal: Convert a snake_case string to PascalCase.
split_by_chars: Split a string by a list of delimiters.
split_once_or_whole: Split s at the first occurrence of sep.
str_aho_corasick_search: Naive multi-pattern search (Aho-Corasick approximation).
str_char_to_string: Convert char to string.
str_concat_assoc_check: Check string concatenation associativity.
str_contains_refl: Check contains reflexivity: s.contains(s).
str_count_alnum: Count ASCII alphanumeric chars.
str_count_whitespace: Count whitespace characters.
str_dec_eq_refl: Check decidable equality: eq(s, s) = true.
str_dec_eq_sym: Check decidable equality symmetry.
str_edit_dist_sym: Check edit distance symmetry: d(a, b) = d(b, a).
str_edit_dist_triangle: Check triangle inequality for edit distance.
str_edit_dist_zero: Check edit distance identity: d(s, s) = 0.
str_ends_with: Check that a string ends with suffix.
str_ext2_aho_corasick_naive
str_ext2_aho_corasick_ty
str_ext2_as_list_char_ty
str_ext2_char_to_string_ty
str_ext2_concat_assoc_ty
str_ext2_concat_left_id_ty
str_ext2_concat_right_id_ty
str_ext2_contains_refl_ty
str_ext2_dec_eq_ty
str_ext2_edit_dist_sym_ty
str_ext2_edit_dist_triangle_ty
str_ext2_edit_dist_zero_ty
str_ext2_ends_with_refl_ty
str_ext2_find_replace_ty
str_ext2_format_parse_ty
str_ext2_hash_consistent_ty
str_ext2_hash_det_ty
str_ext2_join_split_ty
str_ext2_kmp_correct_ty
str_ext2_kmp_failure
str_ext2_lcp_array
str_ext2_lcp_array_ty
str_ext2_length_append_ty
str_ext2_length_empty_ty
str_ext2_lex_lt_irrefl_ty
str_ext2_lex_lt_trans_ty
str_ext2_lex_total_ty
str_ext2_prefix_refl_ty
str_ext2_prefix_trans_ty
str_ext2_rabin_karp_correct_ty
str_ext2_replace_id_ty
str_ext2_slice_len_ty
str_ext2_split_join_ty
str_ext2_starts_with_refl_ty
str_ext2_string_to_nat_ty
str_ext2_substring_ty
str_ext2_suffix_array
str_ext2_suffix_array_sorted_ty
str_ext2_suffix_refl_ty
str_ext2_to_lower_idempotent_ty
str_ext2_to_upper_idempotent_ty
str_ext2_trim_idempotent_ty
str_ext2_unicode_valid_ty
str_ext2_utf8_roundtrip_ty
str_ext2_utf16_len_ty
str_find_replace: Find and replace all occurrences.
str_hash_consistent: Check hash consistency: equal strings have equal hashes.
str_kmp_matches_naive: Check KMP and naive search give same results.
str_kmp_search: KMP pattern search (public wrapper).
str_lcp_array: Build LCP array from suffix array.
str_left_id_check: Check left identity: “” ++ s = s.
str_length_additive: Check length additivity: len(s ++ t) = len(s) + len(t).
str_levenshtein: Compute Levenshtein edit distance (public wrapper).
str_lex_lt: Lexicographic less-than for strings.
str_lex_lt_irrefl: Check lexicographic irreflexivity: ¬(s < s).
str_lex_lt_trans: Check lexicographic transitivity.
str_prefix_refl: Check reflexivity of prefix: s.starts_with(s).
str_prefix_trans: Check transitivity of prefix relation.
str_rabin_karp_matches_kmp: Check Rabin-Karp and KMP give same results.
str_rabin_karp_search: Rabin-Karp pattern search (public wrapper).
str_replace_id: Check replace identity: replace(p, p, s) = s.
str_right_id_check: Check right identity: s ++ “” = s.
str_split_join_roundtrip: Split and join roundtrip: join sep (split sep s) = s.
str_starts_with: Check that a string starts with prefix.
str_substring: Extract a substring by char index and length.
str_suffix_array: Build suffix array for a string.
str_suffix_array_len: Check suffix array has correct length.
str_suffix_array_sorted: Check suffix array is sorted.
str_to_lower_idempotent: Check toLower idempotency.
str_to_upper_idempotent: Check toUpper idempotency.
str_trim_idempotent: Check trim idempotency: trim(trim(s)) = trim(s).
str_unicode_valid: Unicode validity: all bytes form valid UTF-8.
str_utf8_roundtrip: Check UTF-8 roundtrip: decode(encode(s)) = s.
str_utf16_len: Get UTF-16 code unit count.
strip_delimiters: Trim a balanced pair of delimiters from the start and end of s.
strip_line_comment: Remove comments (starting with --) from a line.
strip_prefix: Check whether s starts with prefix, returning the remainder.
strip_suffix: Check whether s ends with suffix, returning the body.
template_format: A simple string formatter that supports {name} template substitution.
title_case: Title-case: capitalize the first letter of each word.
to_lower: Convert a string to lower case.
to_upper: Convert a string to upper case (ASCII only for simplicity).
truncate: Truncate s to at most max_len characters, appending suffix if cut.
word_count: Count the number of words in a string.
word_wrap: Wrap text at width characters, breaking on whitespace.
words: Split text into a list of whitespace-delimited words.

Module functions

Module functions Copy item path

Functions§

Module functions