Struct LeanWorkerStreamingCommand 

pub struct LeanWorkerStreamingCommand<Req, Row, Summary> { /* private fields */ }

A streaming downstream JSON command.

The command names a Lean export with ABI String -> USize -> USize -> IO UInt8. Req, Row, and Summary are downstream-owned serde types. Row and terminal-summary JSON are decoded at the parent boundary, after lean-rs-worker has handled process lifecycle, framing, diagnostics, timeout, cancellation, and completion.

Implementations

impl<Req, Row, Summary> LeanWorkerStreamingCommand<Req, Row, Summary>

pub fn new(export: impl Into<String>) -> Self

Create a typed streaming command for one Lean export.

pub fn export(&self) -> &str

Return the Lean export name used by this command.

Trait Implementations

impl<Req, Row, Summary> Clone for LeanWorkerStreamingCommand<Req, Row, Summary>

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<Req, Row, Summary> Debug for LeanWorkerStreamingCommand<Req, Row, Summary>

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

Formats the value using the given formatter.

impl<Req, Row, Summary> PartialEq for LeanWorkerStreamingCommand<Req, Row, Summary>

fn eq(&self, other: &Self) -> 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<Req, Row, Summary> Eq for LeanWorkerStreamingCommand<Req, Row, Summary>