Skip to main content

lean_alloc_closure

lean_rs_sys::closure

Function lean_alloc_closure 

Source 
pub unsafe fn lean_alloc_closure(
    fun: *mut c_void,
    arity: u32,
    num_fixed: u32,
) -> lean_obj_res
Expand description

Allocate a closure of the requested arity with no captured arguments pre-bound (lean.h:768–777).

§Safety

arity > 0, num_fixed < arity. The returned object has tag LeanClosure, refcount 1, and uninitialized captured-arg storage; the caller must lean_closure_set every captured slot before invoking the closure.

§Panics

Panics if the closure’s total allocation size overflows usize. This is impossible under Lean’s LEAN_CLOSURE_MAX_ARGS == 16 cap; the panic surfaces a runtime invariant breach rather than a recoverable condition.