Module lean_sys::string

source · [−]
Expand description

Strings

Functions

lean_alloc_string⚠
lean_char_default_value

instance : inhabited char := ⟨‘A’⟩

lean_mk_string⚠
lean_mk_string_from_bytes⚠
lean_string_append⚠
lean_string_byte_size⚠
lean_string_capacity⚠
lean_string_cstr⚠
lean_string_data⚠
lean_string_dec_eq⚠
lean_string_dec_lt⚠
lean_string_eq⚠
lean_string_eq_cold⚠
lean_string_hash⚠
lean_string_len⚠
lean_string_length⚠
lean_string_lt⚠
lean_string_mk⚠
lean_string_ne⚠
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_next⚠
lean_string_utf8_prev⚠
lean_string_utf8_set⚠
lean_utf8_n_strlen⚠
lean_utf8_strlen⚠