lean-sys 0.0.3

Bindings to Lean 4's C API
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

/*! External objects */
use crate::*;

#[inline]
pub unsafe fn lean_alloc_external(
    cls: *mut lean_external_class,
    data: *mut c_void,
) -> *mut lean_object {
    let o = lean_alloc_small_object(std::mem::size_of::<lean_external_object>() as c_uint);
    lean_set_st_header(o, LeanExternal as u32, 0);
    (raw_field!(o, lean_external_object, m_class) as *mut *mut lean_external_class).write(cls);
    (raw_field!(o, lean_external_object, m_data) as *mut *mut c_void).write(data);
    o
}

#[inline(always)]
pub unsafe fn lean_get_external_class(o: *mut lean_object) -> *mut lean_external_class {
    *raw_field!(lean_to_external(o), lean_external_object, m_class)
}

#[inline(always)]
pub unsafe fn lean_get_external_data(o: *mut lean_object) -> *mut c_void {
    *raw_field!(lean_to_external(o), lean_external_object, m_data)
}