Expand description
Lifetime-bound owned and borrowed Lean object handles.
Obj is the only safe owner of a Lean reference count inside
lean-rs. Clone performs lean_inc, Drop performs
lean_dec, and both delegate to the pub unsafe fn mirrors in
lean_rs_sys::refcount (the inlined fast paths). ObjRef is the
borrowed view: it costs nothing on construction or drop and cannot
outlive either the runtime borrow or the owning Obj.
Both types are pub(crate); the public handles (LeanExpr<'lean>,
LeanName<'lean>, LeanSession<'lean, '_>, …) wrap them. Raw
lean_* symbols enter this file from lean-rs-sys and never leave
the pub(crate) boundary.