Struct LeanMetaOptions 

pub struct LeanMetaOptions { /* private fields */ }

Bounded options threaded into crate::LeanSession::run_meta.

Construct through Self::new or Default::default and chain the per-field builder methods. Each setter saturates at the same ceiling crate::LeanElabOptions uses; the namespace context is bounded at lean_rs::LEAN_ERROR_MESSAGE_LIMIT.

let opts = LeanMetaOptions::new()
    .heartbeat_limit(50_000)
    .transparency(LeanMetaTransparency::Reducible);

Implementations

impl LeanMetaOptions

pub fn new() -> Self

Construct an options bundle with the documented defaults: empty namespace context, LEAN_HEARTBEAT_LIMIT_DEFAULT heartbeats, LEAN_DIAGNOSTIC_BYTE_LIMIT_DEFAULT bytes of diagnostics, and LeanMetaTransparency::Default reducibility.

pub fn heartbeat_limit(self, heartbeats: u64) -> Self

Replace the heartbeat limit. Values above LEAN_HEARTBEAT_LIMIT_MAX saturate at the ceiling.

pub fn diagnostic_byte_limit(self, bytes: usize) -> Self

Replace the diagnostic byte budget. Values above LEAN_DIAGNOSTIC_BYTE_LIMIT_MAX saturate at the ceiling. Threaded through the ABI; the current single-message failure branches do not actively truncate (Rust’s LeanDiagnostic decoder already bounds at lean_rs::LEAN_ERROR_MESSAGE_LIMIT). Multi-message services would consume the budget the same way the elaboration shim’s serializeMessages does.

pub fn namespace_context(self, ns: &str) -> Self

Replace the namespace context the meta runner opens before evaluating the action (default empty, meaning the imported environment’s root namespace). Long strings truncate at lean_rs::LEAN_ERROR_MESSAGE_LIMIT on a UTF-8 char boundary.

pub fn transparency(self, transparency: LeanMetaTransparency) -> Self

Replace the reducibility setting. Default is LeanMetaTransparency::Default, matching Lean’s Meta default.

Trait Implementations

impl Clone for LeanMetaOptions

fn clone(&self) -> LeanMetaOptions

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanMetaOptions

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

Formats the value using the given formatter.

impl Default for LeanMetaOptions

fn default() -> Self

Returns the “default value” for a type.