Module string

Strings

Functions

lean_alloc_string^⚠

lean_char_default_value

instance : inhabited char := ⟨‘A’⟩

lean_mk_ascii_string_unchecked^⚠

lean_mk_string^⚠

lean_mk_string_from_bytes^⚠

lean_mk_string_from_bytes_unchecked^⚠

lean_mk_string_unchecked^⚠

lean_string_append^⚠

lean_string_byte_size^⚠

lean_string_capacity^⚠

lean_string_cstr^⚠

lean_string_data^⚠

lean_string_data_byte_size^⚠

lean_string_dec_eq^⚠

lean_string_dec_lt^⚠

lean_string_eq^⚠

lean_string_eq_cold^⚠

lean_string_get_byte_fast^⚠

lean_string_hash^⚠

lean_string_len^⚠

lean_string_length^⚠

lean_string_lt^⚠

lean_string_mk^⚠

lean_string_ne^⚠

lean_string_of_usize^⚠

lean_string_push^⚠

lean_string_size^⚠

lean_string_utf8_at_end^⚠

lean_string_utf8_byte_size^⚠

lean_string_utf8_extract^⚠

lean_string_utf8_get^⚠

lean_string_utf8_get_fast^⚠

lean_string_utf8_get_fast_cold^⚠

lean_string_utf8_next^⚠

lean_string_utf8_next_fast^⚠

lean_string_utf8_next_fast_cold^⚠

lean_string_utf8_prev^⚠

lean_string_utf8_set^⚠

lean_utf8_n_strlen^⚠

lean_utf8_strlen^⚠