Struct LeanWorkerElabOptions 

pub struct LeanWorkerElabOptions { /* private fields */ }

Bounded elaboration options for worker-session requests.

This mirrors the stable knobs from lean-rs-host::LeanElabOptions without exposing the in-child host object itself across the process boundary.

Implementations

impl LeanWorkerElabOptions

pub fn new() -> Self

Create worker elaboration options with lean-rs-host defaults.

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

Replace the namespace context.

pub fn file_label(self, label: &str) -> Self

Replace the diagnostic file label.

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

Replace the heartbeat limit. The child applies the host ceiling.

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

Replace the diagnostic byte limit. The child applies the host ceiling.

Trait Implementations

impl Clone for LeanWorkerElabOptions

fn clone(&self) -> LeanWorkerElabOptions

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanWorkerElabOptions

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

Formats the value using the given formatter.

impl Default for LeanWorkerElabOptions

fn default() -> Self

Returns the “default value” for a type.

impl PartialEq for LeanWorkerElabOptions

fn eq(&self, other: &LeanWorkerElabOptions) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for LeanWorkerElabOptions

impl StructuralPartialEq for LeanWorkerElabOptions