Skip to main content

lean_alloc_ctor

lean_rs_sys::ctor

Function lean_alloc_ctor 

Source 
pub unsafe fn lean_alloc_ctor(
    tag: u8,
    num_objs: u8,
    scalar_sz: usize,
) -> lean_obj_res
Expand description

Allocate a freshly initialized constructor object — Rust mirror of lean_alloc_ctor (lean.h:659–664).

tag selects the constructor (0..=LEAN_MAX_CTOR_TAG), num_objs names how many object-pointer fields it carries, and scalar_sz is the byte width of the appended scalar payload. The returned object has m_rc=1; the caller subsequently initialises every object field via lean_ctor_obj_cptr writes and every scalar field via lean_ctor_set_*.

§Safety

All three sizing parameters must fit lean.h’s LEAN_MAX_CTOR_TAG / LEAN_MAX_CTOR_FIELDS / LEAN_MAX_CTOR_SCALARS_SIZE ceilings. The caller must fully initialise every declared field before passing the object to other Lean routines (notably the object-pointer fields, which Lean’s RC machinery will otherwise read as garbage).