Struct Obj 

pub struct Obj<'lean> { /* private fields */ }

Owned handle to a Lean heap or scalar object.

Obj<'lean> holds exactly one Lean reference count for the duration of its scope. Clone bumps that count via lean_inc; Drop releases it via lean_dec. The 'lean lifetime parameter is the type-system anchor for “init-before-use”: the constructor takes a &'lean LeanRuntime borrow, so the handle cannot exist before the runtime is up and cannot outlive the borrow it was derived from.

Neither Send nor Sync: the contained NonNull<lean_object> and the PhantomData<&'lean LeanRuntime> (where LeanRuntime: !Sync) both propagate the per-thread restriction. A negative-bound static assertion in tests fails to compile if either auto-trait is ever implemented.

Implementations

impl<'lean> Obj<'lean>

pub unsafe fn from_owned_raw( _runtime: &'lean LeanRuntime, ptr: *mut lean_object, ) -> Self

Wrap a raw owned Lean pointer.

Safety

The caller must guarantee all of the following:

• ptr is non-null and points to a live Lean object (a scalar-tagged pointer is allowed; lean_inc / lean_dec short-circuit on those).
• The caller transfers exactly one Lean reference count to this handle. After this call the caller must not call lean_dec on ptr itself; releasing the count is the new Obj’s job (via Drop or Obj::into_raw).
• ptr was produced by the same Lean runtime instance witnessed by _runtime. The borrow is a type-level proof that Lean is initialised and pins the 'lean lifetime of the returned handle; it carries no payload of its own.

pub fn into_raw(self) -> *mut lean_object

Consume the handle and return the underlying raw owned pointer without running Drop.

The returned pointer carries the same one reference count that this Obj held. Whoever receives it inherits the obligation to release it (via lean_dec, or by reconstructing an Obj with Obj::from_owned_raw).

pub fn as_raw_borrowed(&self) -> *mut lean_object

Borrow the underlying raw pointer for a borrowed-argument FFI call (b_lean_obj_arg).

The returned pointer must not be passed where a Lean function expects to consume one reference count; that is what Obj::into_raw is for.

pub fn borrow(&self) -> ObjRef<'lean, '_>

Produce a borrowed view tied to this Obj.

pub fn runtime(&self) -> &'lean LeanRuntime

Recover the runtime borrow that anchors this handle’s 'lean.

LeanRuntime is a ZST whose only construction path goes through LeanRuntime::init; the 'lean lifetime carried by self is already a witness that a runtime borrow is live in the caller’s scope. Container readers (e.g. Vec<T>::try_from_lean) use this to wrap extracted fields as fresh Obj<'lean> values without forcing the runtime through every signature in the trait surface.

&self rather than an associated function because the borrow pins the inferred 'lean lifetime to this Obj’s lifetime — callers do not need to spell the parameter out at the call site.

Trait Implementations

impl Clone for Obj<'_>

fn clone(&self) -> Self

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Obj<'_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Drop for Obj<'_>

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.

impl<'lean> LeanAbi<'lean> for Obj<'lean>

type CRepr = *mut lean_object

The C-ABI type Lake emits for this Lean type at function signatures.

impl<'lean> TryFromLean<'lean> for Obj<'lean>

fn try_from_lean(obj: Self) -> LeanResult<Self>

Decode obj into Self, returning a LeanError::Host with stage HostStage::Conversion if the object’s kind or payload is outside the type’s representable range.