Module external 

External objects — externs and inline accessors from lean.h:295–1332.

Functions

lean_alloc_external^⚠

Allocate an external-data wrapper (lean.h:1307–1313).

lean_get_external_class^⚠

Read the external object’s class pointer (lean.h:1315–1317).

lean_get_external_data^⚠

Read the external object’s data pointer (lean.h:1319–1321).

lean_register_external_class^⚠

Register an external-object class. The returned pointer outlives the process; the runtime does not free registered classes (lean.h:303).

Type Aliases

lean_external_finalize_proc

Finalizer signature stored in a lean_external_class (lean.h:295).

lean_external_foreach_proc

Foreach signature stored in a lean_external_class (lean.h:296).