Struct ProofReport 

struct ProofReport {
    axioms: Option<String>,
    errors: Vec<String>,
}

What lake build reported about the external proof of a single function

Fields

axioms: Option<String>

The message of the #print axioms in the checking file, if it was elaborated

errors: Vec<String>

Errors reported in the checking or proof file

Implementations

impl ProofReport

fn status( self, checking_file: &str, sorries: &[String], ) -> Result<(), Vec<String>>

The proof is accepted iff the checking file was elaborated (witnessed by the info message of its #print axioms), neither the checking nor the proof file report errors, and the proof does not depend on sorryAx, i.e., neither the proof nor any lemma it (transitively) uses has a sorry. On failure, returns the relevant messages reported by lean, where sorries are all the sorry warnings in the build (one of which is the culprit for a sorryAx).

Trait Implementations

impl Default for ProofReport

fn default() -> Self

Returns the “default value” for a type.