Function alloc_ctor_with_objects 

pub fn alloc_ctor_with_objects<'lean, const N: usize>(
    runtime: &'lean LeanRuntime,
    tag: u8,
    objects: [Obj<'lean>; N],
) -> Obj<'lean>

Allocate a freshly-initialised constructor with N object-pointer fields and no scalar payload.

tag is the inductive constructor index (Lean’s declaration order: Option.none = 0, Option.some = 1, Except.error = 0, Except.ok = 1, …). Each entry of objects is moved into its slot via Obj::into_raw, so the returned Obj owns the only live refcount per field plus its own header count. The const-generic N matches the number of object-pointer slots the Lean inductive declares, which keeps the call site self-documenting and lets the compiler refuse arity mismatches.

Panics

Panics only via lean_alloc_ctor’s strict_* arithmetic overflow guard — unreachable for the constructor shapes Lean emits (LEAN_MAX_CTOR_FIELDS = 256).