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

Function lean_get_external_data

src/external.rs:22–24  ·  view source on GitHub ↗
(o: *mut lean_object)

Source from the content-addressed store, hash-verified

20
21#[inline(always)]
22pub unsafe fn lean_get_external_data(o: *mut lean_object) -> *mut c_void {
23 *raw_field!(lean_to_external(o), lean_external_object, m_data)
24}
25
26#[inline(always)]
27pub unsafe fn lean_set_external_data(o: *mut lean_object, data: *mut c_void) -> *mut lean_object {

Callers

nothing calls this directly

Calls

no outgoing calls

Tested by

no test coverage detected