Module object 

Object inspection and allocation helpers — mirrors lean.h:312–630.

Covers scalar-pointer encoding (lean_is_scalar), tag reads, the lean_is_* predicates, the lean_to_* casts (returned as raw *mut lean_object for opacity), and the runtime-mode reads (lean_is_st, lean_is_mt, lean_is_persistent, lean_is_exclusive, lean_is_shared). Allocation primitives exported by libleanshared (lean_alloc_object, lean_free_object) are declared here; the higher-level inline allocators (lean_alloc_ctor, lean_alloc_closure, lean_alloc_array, …) live in their category modules.

Functions

lean_alloc_object^⚠

Allocate an uninitialized Lean heap object of size sz bytes (lean.h:490). The caller is responsible for initializing the header via lean_set_st_header-equivalent writes, which only this crate’s helpers should perform.

lean_box^⚠

Box an unsigned integer into a scalar Lean object (lean.h:313).

lean_free_object^⚠

Free a Lean heap object previously allocated with lean_alloc_object (lean.h:491).

lean_is_array^⚠

True if o is an object array (lean.h:567).

lean_is_closure^⚠

True if o is a closure object (lean.h:566).

lean_is_ctor^⚠

Constructor objects share tags 0..=LEAN_MAX_CTOR_TAG; this is the lean_is_ctor predicate from lean.h:565.

lean_is_exclusive^⚠

True if o is single-threaded with refcount exactly one (lean.h:592–598).

lean_is_external^⚠

True if o is an external object (lean.h:574).

lean_is_mpz^⚠

True if o is an MPZ (big integer) object (lean.h:570).

lean_is_mt^⚠

Multi-threaded test (lean.h:515–517).

lean_is_persistent^⚠

Persistent test (lean.h:524–526).

lean_is_promise^⚠

True if o is a promise object (lean.h:573).

lean_is_ref^⚠

True if o is a Lean Ref object (lean.h:575).

lean_is_sarray^⚠

True if o is a scalar array (lean.h:568).

lean_is_scalar^⚠

Scalar-pointer test (lean.h:312). Scalar values are tagged with the low bit set; the pointer never aliases a real allocation.

lean_is_shared^⚠

True if o is single-threaded with refcount > 1 (lean.h:604–610).

lean_is_st^⚠

Single-threaded test (lean.h:519–521).

lean_is_string^⚠

True if o is a string (lean.h:569).

lean_is_task^⚠

True if o is a task object (lean.h:572).

lean_is_thunk^⚠

True if o is a thunk object (lean.h:571).

lean_obj_tag^⚠

Read the object’s “logical” tag (lean.h:577–579): for scalar values this is the unboxed payload; otherwise it is the heap tag.

lean_object_byte_size^⚠

Total byte size of o’s allocation (lean.h:506).

lean_object_data_byte_size^⚠

Byte size of o’s salient (initialized) storage (lean.h:513).

lean_ptr_other^⚠

Read the object’s m_other byte (lean.h:497–499).

lean_ptr_tag^⚠

Read the object’s tag byte (lean.h:493–495).

lean_unbox^⚠

Unbox a scalar Lean object (lean.h:314).