Struct AxiomUsage

Source

pub struct AxiomUsage {
    pub axioms: BTreeSet<String>,
    pub unresolved: BTreeSet<String>,
}

Expand description

What a proof rests on: the axioms it cites transitively, and the names that resolve to nothing.

Fields§

§axioms: BTreeSet<String>

Axioms cited, TRANSITIVELY through definitions. Sorted, so a report is stable and diffable.

§unresolved: BTreeSet<String>

Names that resolve to NOTHING in the context checked against. Non-empty means the proof was minted against a larger base than the one re-checking it — trusted-base drift, named.

Implementations§

Source §

impl AxiomUsage

Source

pub fn absorb(&mut self, other: AxiomUsage)

Fold another report into this one — the union, on both halves.

A closure is almost never over one term: a declaration is its TYPE and its BODY, and a certificate is its proof term and the proposition it CLAIMS. Every caller that walks two terms goes through here, so no caller can merge the axioms and forget the unresolved names — the half that reports trusted-base DRIFT, and the half a summary is most tempted to drop.

Source

pub fn beyond(&self, permitted: &[&str]) -> BTreeSet<String>

Does this proof rest on anything outside permitted?

A trust POLICY is written from this, so it counts an unresolved name too — see AxiomUsage::cited. Permitting a name by spelling silences it whichever half it is in, so one list governs both.

Source

pub fn admitted(&self) -> BTreeSet<String>

Every ADMITTED name this proof rests on, transitively — the taint.

Better than Lean here, and deliberately: Lean warns on the declaration that CONTAINS the sorry and says nothing about its dependants, so a theorem three lemmas downstream of an admission looks finished and #print axioms is a command you have to remember to run. This reads the closure, so the taint is a property of the proof rather than of a warning you might have missed, and it cannot be lost by renaming, re-exporting or citing at a distance.

Source

pub fn is_admitted(&self) -> bool

Is this proof tainted by an admission? Sugar for !admitted().is_empty().

Source

pub fn is_tainted_by(&self, admitted: &[&str]) -> bool

A proof that cites any name a caller considers admitted is not a proof, and neither is anything that transitively cites it.

Source

pub fn render(&self, subject: &str) -> String

The #print axioms report, rendered. One line, stable, diffable — and it names the admission FIRST when there is one, because that is the part a reader must not scroll past.