Module string 

String objects — externs and inline accessors from lean.h:1157–1234.

Functions

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^⚠

Total allocation footprint of o (lean.h:1170).

lean_string_capacity^⚠

m_capacity field (lean.h:1169).

lean_string_cstr^⚠

Pointer to the string’s NUL-terminated UTF-8 bytes (lean.h:1178–1181).

lean_string_data^⚠

lean_string_eq_cold^⚠

lean_string_hash^⚠

lean_string_len^⚠

m_length field — UTF-8 character count (lean.h:1183).

lean_string_lt^⚠

lean_string_mk^⚠

lean_string_push^⚠

lean_string_size^⚠

m_size field — byte length including the trailing \0 (lean.h:1182).

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^⚠