MCPcopy Create free account
hub / github.com/digama0/lean-sys / lean_char_default_value

Function lean_char_default_value

src/string.rs:27–29  ·  view source on GitHub ↗
()

Source from the content-addressed store, hash-verified

25/** instance : inhabited char := ⟨'A'⟩ */
26#[inline(always)]
27pub fn lean_char_default_value() -> c_char {
28 'A' as c_char
29}
30
31#[inline(always)]
32pub unsafe fn lean_string_cstr(o: b_lean_obj_arg) -> *const u8 {

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected