Struct lean_object 

pub struct lean_object { /* private fields */ }

Opaque handle to a Lean 4 heap object.

lean_object is only ever held by pointer. The published type is zero-sized + !Send + !Sync + !Unpin, so downstream code cannot read or write the underlying header (m_rc, m_tag, …) directly. Reach object state through this crate’s pub unsafe fn helpers.

The C struct in lean.h:131–136 is { int m_rc; unsigned m_cs_sz:16; unsigned m_other:8; unsigned m_tag:8; } for 8 total bytes. A crate- private LeanObjectRepr mirrors that layout; the digest pinned at build time guarantees the C and Rust pictures match.