Module types 

Opaque lean_object plus the calling-convention typedefs from lean.h:131–168.

Structs

lean_object

Opaque handle to a Lean 4 heap object.

Type Aliases

b_lean_obj_arg

“Borrowed” object argument — caller retains the refcount.

b_lean_obj_res

“Borrowed” object result — refcount belongs to a longer-lived owner.

lean_obj_arg

“Standard” object argument — caller transfers ownership of one refcount.

lean_obj_res

“Standard” object result — callee returns a fresh owned refcount.

u_lean_obj_arg

“Unique” object argument — caller asserts the object is non-shared.