Module closure 

Closure objects — externs and inline accessors from lean.h:762–813.

Functions

lean_alloc_closure^⚠

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

lean_apply_1^⚠

lean_apply_2^⚠

lean_apply_3^⚠

lean_apply_4^⚠

lean_apply_5^⚠

lean_apply_6^⚠

lean_apply_7^⚠

lean_apply_8^⚠

lean_apply_9^⚠

lean_apply_10^⚠

lean_apply_11^⚠

lean_apply_12^⚠

lean_apply_13^⚠

lean_apply_14^⚠

lean_apply_15^⚠

lean_apply_16^⚠

lean_apply_m^⚠

Apply a closure to n arguments, where n > 16.

lean_apply_n^⚠

Apply a closure to n arguments, where n <= 16.

lean_closure_arg_cptr^⚠

Pointer to the closure’s captured-argument array (lean.h:767).

lean_closure_arity^⚠

Arity of the closure’s underlying function (lean.h:765).

lean_closure_fun^⚠

Code pointer of the closure (lean.h:764).

lean_closure_get^⚠

Read the i-th captured argument (lean.h:778).

lean_closure_num_fixed^⚠

Number of arguments already captured in the closure (lean.h:766).

lean_closure_set^⚠

Write the i-th captured argument (lean.h:782).