Struct AxiomFootprint 

pub struct AxiomFootprint {
    pub trusted: Vec<String>,
    pub introduced: Vec<String>,
}

What a certified proof term actually RESTS ON — the #print axioms analogue.

Two kernels give ZERO protection against an added axiom: double_check asks both the same question against the same context, so double_check(ctx, sorryAx (2 = 3)) returns Agreed. The only thing that catches an admission is asking what the proof term CITES and comparing that against a freshly rebuilt trusted base — which is what this report does.

The split is the point. trusted is the part of the prelude the proof used, so a classical theorem is distinguishable from a constructive one by reading its certificate rather than its prose. introduced is everything else the term cites: this theorem’s premise hypotheses and symbols — and anything smuggled into the context, which is the slot a sorryAx lands in.

Fields

trusted: Vec<String>

Declarations the term cites that a freshly-registered StandardLibrary also declares, with the same type: the trusted base this proof used. Sorted, deduplicated.

introduced: Vec<String>

Declarations the term cites that a rebuilt prelude does NOT declare (or declares at a different type). Sorted, deduplicated.

Trait Implementations

impl Clone for AxiomFootprint

fn clone(&self) -> AxiomFootprint

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AxiomFootprint

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

Formats the value using the given formatter.

impl Default for AxiomFootprint

fn default() -> AxiomFootprint

Returns the “default value” for a type.

impl PartialEq for AxiomFootprint

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

impl StructuralPartialEq for AxiomFootprint