pub struct ObjView<'lean, 'a> { /* private fields */ }Expand description
Borrowed, allocation-free inspection view over an existing Lean object.
This is the host-facing boundary for Lean’s scalar/nullary and
constructor-object representation. Callers can ask whether a value is
scalar-tagged, read a scalar constructor tag, or narrow to
CtorView before reading constructor header and scalar-tail fields.
The view never transfers ownership and never exposes the underlying
lean_object*.
Implementations§
Source§impl<'lean, 'a> ObjView<'lean, 'a>
impl<'lean, 'a> ObjView<'lean, 'a>
Sourcepub fn scalar_payload(&self, label: &str) -> LeanResult<usize>
pub fn scalar_payload(&self, label: &str) -> LeanResult<usize>
Read the payload of a scalar-tagged object.
This is the representation Lean uses for nullary-only inductive
values and for some small primitive values (Nat, Bool, Unit
in boxed positions). The caller supplies label only for the
error message; it is not touched on the success path.
§Errors
Returns a conversion error if the object is heap-allocated.
Sourcepub fn sum_tag(&self) -> LeanResult<u8>
pub fn sum_tag(&self) -> LeanResult<u8>
Read a sum-constructor tag encoded either as a scalar nullary tag or as a heap constructor tag.
This matches Lean’s mixed-inductive ABI rule: nullary constructors can be scalar-tagged, while constructors with fields are heap ctors. The returned tag is the Lean declaration-order constructor index.
§Errors
Returns a conversion error if the object is heap-allocated but is
not a constructor, or if a scalar payload does not fit in u8.
Sourcepub fn ctor(&self) -> LeanResult<CtorView<'lean, 'a>>
pub fn ctor(&self) -> LeanResult<CtorView<'lean, 'a>>
Narrow this object to a heap-constructor view.
§Errors
Returns a conversion error if the object is scalar-tagged or is a non-constructor heap object.
Sourcepub fn ctor_shape(
&self,
expected_tag: u8,
expected_num_object_fields: usize,
label: &str,
) -> LeanResult<CtorView<'lean, 'a>>
pub fn ctor_shape( &self, expected_tag: u8, expected_num_object_fields: usize, label: &str, ) -> LeanResult<CtorView<'lean, 'a>>
Narrow this object to a constructor with the expected tag and object-slot count.
This is the common generated-result shape check. It validates the
constructor tag and object-field arity before any caller reads
scalar-tail values or consumes fields through take_ctor_objects.
§Errors
Returns a conversion error if the object is not a constructor, or if the constructor tag or object-field count differs.