Struct Certificate 

pub struct Certificate {
    pub proof_term: Term,
    pub claimed_type: Term,
    pub prelude_version: String,
}

A self-contained, re-checkable proof certificate.

proof_term is claimed to have type claimed_type in the standard prelude context. Nothing else is trusted: the re-checker supplies its own axioms.

Fields

proof_term: Term

The proof (a lambda-calculus term).

claimed_type: Term

The proposition the proof claims to establish (a type).

prelude_version: String

The axiom-set version this certificate was produced against.

Implementations

impl Certificate

pub fn new(proof_term: Term, claimed_type: Term) -> Self

Bundle a proof term with the proposition it claims to prove.

pub fn axioms_used(&self) -> AxiomUsage

The axioms this certificate’s proof actually rests on — our #print axioms.

Computed against the trusted base the certificate would be RE-CHECKED in, which is the only context whose answer is worth anything: a closure taken against the minting side’s environment reports what the prover believed, not what the verifier is being asked to accept.

Over the proof term AND the claimed type, because a certificate is both. An axiom named in the theorem’s own STATEMENT is a real dependency — Π(h : Nonempty Nat). Eq Nat (Classical_choice Nat h) Zero rests on choice whatever the proof term looks like — and Lean reports it: CollectAxioms visits a constant’s type as well as its value.

Trait Implementations

impl Clone for Certificate

fn clone(&self) -> Certificate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Certificate

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Certificate

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for Certificate

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

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Certificate