Module ctor 

Constructor objects and polymorphic boxing — Rust mirrors of lean.h:642–760 and the lean_box_uint* / lean_box_float family at lean.h:2811–2873.

Lean’s polymorphic boxing for fixed-width unboxed values (UInt32 on 32-bit, UInt64, USize, Float, Float32) wraps the value in a single-field constructor (tag=0, num_objs=0, scalar payload sized for the value). The boxed form is the representation an Array UIntN / Option UIntN / Except E UIntN field carries; the direct unboxed form is reserved for argument and return positions in exported Lean functions.

Each helper here threads through the lean_alloc_object extern declared in crate::object and writes header bytes via the crate-private LeanCtorObjectRepr layout in crate::repr. The pinned EXPECTED_HEADER_DIGEST guarantees the field offsets match the active lean.h.

Functions

lean_alloc_ctor^⚠

Allocate a freshly initialized constructor object — Rust mirror of lean_alloc_ctor (lean.h:659–664).

lean_box_float^⚠

Box an f64 as a single-field constructor (lean.h:2855–2859).

lean_box_uint32^⚠

Box a u32 as a single-field constructor (lean.h:2813–2823).

lean_box_uint64^⚠

Box a u64 as a single-field constructor (lean.h:2835–2839).

lean_box_usize^⚠

Box a usize as a single-field constructor (lean.h:2845–2849).

lean_ctor_get_float^⚠

Read an f64 field at byte offset within the scalar payload (lean.h:717–720).

lean_ctor_get_uint8^⚠

Read a u8 field at byte offset within the scalar payload (lean.h:697–700).

lean_ctor_get_uint16^⚠

Read a u16 field at byte offset within the scalar payload (lean.h:702–705).

lean_ctor_get_uint32^⚠

Read a u32 field at byte offset within the scalar payload (lean.h:707–710).

lean_ctor_get_uint64^⚠

Read a u64 field at byte offset within the scalar payload (lean.h:712–715).

lean_ctor_get_usize^⚠

Read a usize field stored after the object-pointer slots (lean.h:692).

lean_ctor_num_objs^⚠

Number of object-pointer fields stored in a constructor (lean.h:644).

lean_ctor_obj_cptr^⚠

Pointer to the constructor’s object-field storage (lean.h:649–652).

lean_ctor_scalar_cptr^⚠

Pointer to the constructor’s scalar payload storage (lean.h:654–657). Sits immediately past the object-pointer slots.

lean_ctor_set_float^⚠

Write an f64 field at byte offset within the scalar payload (lean.h:752–755).

lean_ctor_set_uint8^⚠

Write a u8 field at byte offset within the scalar payload (lean.h:732–735).

lean_ctor_set_uint16^⚠

Write a u16 field at byte offset within the scalar payload (lean.h:737–740).

lean_ctor_set_uint32^⚠

Write a u32 field at byte offset within the scalar payload (lean.h:742–745).

lean_ctor_set_uint64^⚠

Write a u64 field at byte offset within the scalar payload (lean.h:747–750).

lean_ctor_set_usize^⚠

Write a usize field at slot i (counted in usize units past the object-pointer slots) — mirror of lean.h:727–730.

lean_unbox_float^⚠

Recover the f64 payload from a constructor produced by lean_box_float (lean.h:2861–2863).

lean_unbox_uint32^⚠

Recover the u32 payload from a constructor produced by lean_box_uint32 (lean.h:2825–2833).

lean_unbox_uint64^⚠

Recover the u64 payload from a constructor produced by lean_box_uint64 (lean.h:2841–2843).

lean_unbox_usize^⚠

Recover the usize payload from a constructor produced by lean_box_usize (lean.h:2851–2853).