Struct LeanProgressTick 

pub struct LeanProgressTick {
    pub current: u64,
    pub total: u64,
}

Counter payload for progress-like callback ticks.

lean-rs-host maps this payload into host progress events; lean-rs itself attaches no theorem-prover policy to the counters.

Fields

current: u64

Current item, tick, or phase-local counter supplied by Lean.

total: u64

Total item count or phase-local bound supplied by Lean.

Trait Implementations

impl Clone for LeanProgressTick

fn clone(&self) -> LeanProgressTick

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanProgressTick

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

Formats the value using the given formatter.

impl PartialEq for LeanProgressTick

fn eq(&self, other: &LeanProgressTick) -> 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 Copy for LeanProgressTick

impl Eq for LeanProgressTick

impl LeanCallbackPayload for LeanProgressTick

impl StructuralPartialEq for LeanProgressTick