Enum LeanEvidence 

pub enum LeanEvidence {
    NotObserved,
    Accepted {
        axioms: Vec<String>,
        sources: BTreeMap<String, Vec<u8>>,
        toolchain: String,
        exporter: String,
    },
}

What the run observed of Lean itself.

Variants

NotObserved

A pre-exported artifact: Lean was not run, so its acceptance is not established.

Accepted

Lean compiled the project in isolation, and #print axioms reported axioms (Lean names) for the target.

Fields

axioms: Vec<String>

sources: BTreeMap<String, Vec<u8>>

The original Lean sources, by project-relative path (published under source/).

toolchain: String

The pinned toolchain and exporter identities.

exporter: String

Trait Implementations

impl Clone for LeanEvidence

fn clone(&self) -> LeanEvidence

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanEvidence

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

Formats the value using the given formatter.

impl PartialEq for LeanEvidence

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

impl StructuralPartialEq for LeanEvidence