Struct Inventory 

pub struct Inventory {
    pub items: Vec<InventoryItem>,
    pub summary: InventorySummary,
}

The whole inventory: every classified claim plus its rolled-up summary.

Fields

items: Vec<InventoryItem>

summary: InventorySummary

Implementations

impl Inventory

pub fn from_run_report(report: &RunReport) -> Inventory

Classify every claim in a largo test RunReport — examples and finite-enumeration properties. Skipped tests carry no verified claim, so they are not inventoried as passing or failing evidence.

impl Inventory

pub fn from_prove( theorems: &[ProvenClaim], axioms: &[String], admitted: &[String], ) -> Result<Inventory, String>

Build the inventory for a largo prove pass from its classified claims: theorems, axioms (assumptions), and admitted assumptions. REJECTS a name that appears both as a theorem and as an axiom/admitted assumption — an axiom must never be able to masquerade as a proved theorem.

axioms and admitted are (name) lists; theorems are ProvenClaims. Returns Err(collision_message) naming every colliding name, so the run can fail loud.

Trait Implementations

impl Clone for Inventory

fn clone(&self) -> Inventory

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Inventory

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

Formats the value using the given formatter.

impl Serialize for Inventory

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

where __S: Serializer,

Serialize this value into the given Serde serializer.