Struct TheoremCertificate 

pub struct TheoremCertificate {
    pub theorem: String,
    pub proof_term: Term,
    pub claimed_type: Term,
    pub declarations: Vec<CertDeclaration>,
    pub definitions: Vec<CertDefinition>,
    pub prelude_version: String,
}

A self-contained, re-checkable certificate for a theorem proved FROM premises.

proof_term is claimed to have type claimed_type in the standard prelude EXTENDED by the disclosed declarations (assumptions) and definitions (transparent). The re-checker rebuilds the prelude itself and replays only this disclosed delta, then type-checks — it never trusts, or even sees, how the proof was found.

Fields

theorem: String

The theorem’s identity (its ## Theorem: Name), for provenance in reports.

proof_term: Term

The proof (a lambda-calculus term).

claimed_type: Term

The proposition the proof claims to establish (a type) — the theorem’s goal.

declarations: Vec<CertDeclaration>

The disclosed premise hypotheses + declared vocabulary the proof assumes. Every assumption the theorem rests on is enumerated here, in the open.

definitions: Vec<CertDefinition>

The disclosed transparent definitions the proof unfolds.

prelude_version: String

The axiom-set version this certificate was produced against.

Implementations

impl TheoremCertificate

pub fn axioms_used(&self) -> AxiomUsage

The axioms this certificate’s proof actually rests on, re-computed against the trusted base it would be re-checked in — NOT against whatever the minting side chose to disclose.

Over the proof term AND the claimed goal, for the same reason Certificate::axioms_used is: the statement is half of what a certificate asserts, and an assumption it names is one the reader is being asked to accept. A report that walked only the proof term would say a theorem ABOUT Classical_choice rests on nothing, and axiom_dependencies_of — the door the REPL comes in by — already answers the same question the other way, so the two doors would disagree about one graph.

impl TheoremCertificate

pub fn new( theorem: impl Into<String>, proof_term: Term, claimed_type: Term, declarations: Vec<CertDeclaration>, definitions: Vec<CertDefinition>, ) -> Self

Bundle a proof term, its goal, and the disclosed environment delta.

Trait Implementations

impl Clone for TheoremCertificate

fn clone(&self) -> TheoremCertificate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TheoremCertificate

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for TheoremCertificate

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for TheoremCertificate

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

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 TheoremCertificate