Struct Hyp 

pub struct Hyp {
    pub name: String,
    pub prop: ProofExpr,
    /* private fields */
}

A local hypothesis: its name, its proposition prop, and proof — a derivation that proves prop in the current local context. For a hypothesis that is directly in scope (a premise, an intro-discharged antecedent, or a branch hypothesis bound by cases) the proof is a PremiseMatch leaf the certifier resolves against the bound/registered hypothesis. For a conjunct extracted by cases from A ∧ B, the proof is the ConjunctionElim PROJECTION of the parent — so using the conjunct emits the projection, not a dangling reference. This is what lets elimination compose with the rest.

Fields

name: String

prop: ProofExpr

Trait Implementations

impl Clone for Hyp

fn clone(&self) -> Hyp

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Hyp

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

Formats the value using the given formatter.