pub unsafe fn lean_dec_ref(o: *mut lean_object)Expand description
Decrement o’s refcount, taking the cold path to free if it reaches zero
(lean.h:554–560).
§Safety
o must be a valid non-scalar Lean heap object. The runtime invariant
that m_rc == 0 means “persistent, no refcounting” is honoured: this
function is a no-op in that case.
§Panics
The single-threaded fast path only runs when m_rc > 1, so subtracting
1 cannot underflow; the panic guard exists to catch a future invariant
breach (e.g. unsynchronized concurrent mutation) rather than a
recoverable condition.