Struct ProofCertificate 

pub struct ProofCertificate {
    pub proposition: Expr,
    pub proof_term: Expr,
    pub is_constructive: bool,
    pub has_sorry: bool,
}

A proof certificate: a self-contained record attesting that a term is a valid proof of a proposition.

Fields

proposition: Expr

The proven proposition.

proof_term: Expr

The proof term.

is_constructive: bool

Whether the proof is constructive.

has_sorry: bool

Whether the proof contains any sorry.

Implementations

impl ProofCertificate

pub fn new(proposition: Expr, proof_term: Expr) -> Self

Create a certificate from a proposition and proof term.

pub fn is_trusted(&self) -> bool

Whether this certificate is fully trusted (no sorry, constructive).

Trait Implementations

impl Clone for ProofCertificate

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofCertificate

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

Formats the value using the given formatter.