Struct CtorView 

pub struct CtorView<'lean, 'a> { /* private fields */ }

Borrowed view of a heap-allocated Lean constructor.

Constructed only after ObjView::ctor has verified that the source object is a constructor. The cached header facts make repeated reads cheap and keep scalar-tail bounds checks explicit at each offset.

Implementations

impl<'lean, 'a> CtorView<'lean, 'a>

pub fn tag(&self) -> u8

Constructor tag in Lean declaration order.

pub fn uint8(&self, offset: u32, label: &str) -> LeanResult<u8>

Read a UInt8 field from the constructor scalar tail at byte offset.

Errors

Returns a conversion error if the requested byte range is outside the scalar tail.

pub fn uint64(&self, offset: u32, label: &str) -> LeanResult<u64>

Read a UInt64 field from the constructor scalar tail at byte offset.

Errors

Returns a conversion error if the requested byte range is outside the scalar tail.

pub fn bool(&self, offset: u32, label: &str) -> LeanResult<bool>

Decode a Bool-encoded scalar-tail byte.

Errors

Returns a conversion error if the byte is outside the scalar tail or is not 0 / 1.

Trait Implementations

impl<'lean, 'a> Clone for CtorView<'lean, 'a>

fn clone(&self) -> CtorView<'lean, 'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'lean, 'a> Copy for CtorView<'lean, 'a>