Struct CommittedLemma 

pub struct CommittedLemma {
    pub name: String,
    pub text: String,
    pub embed: bool,
    pub provenance: LemmaProvenance,
}

A lemma available to a law’s proof: its theorem name plus Lean text (statement, and for embedded ones the tactic too). Two provenances flow through the same orientation / loop-exclusion / simp-selection machinery:

• embedded (embed = true) — a kernel-proved lemma parsed back from a committed DiscoveredLemmas.lean; its full text is written into the generated proof project (re-proved in the same lake build).
• reference (embed = false) — an already-proved EARLIER user verify … law in the same file (część A): its theorem is already emitted, so only the NAME joins later laws’ simp sets; text carries just the synthesized theorem <name> : <lhs> = <rhs> statement, used for orientation + loop analysis, never written out.

Fields

name: String

text: String

embed: bool

Write text verbatim into the proof project (true), or only reference name in simp sets because it is already emitted (false).

provenance: LemmaProvenance

Which proposer ORIGINATED this lemma (orthogonal to embed/strength). Carried so the future Lemma-Calculation path can set it; every current producer is the discovery enumerator, so this is always LemmaProvenance::Enumerated for now.

Implementations

impl CommittedLemma

pub fn reference(name: String, text: String) -> Self

A reference to an already-emitted theorem (an earlier user law) — name plus synthesized statement, never written out. text should be a well-formed theorem <name> : <stmt> := by head so the shared orientation / loop analysis reads it like any other lemma.

Trait Implementations

impl Clone for CommittedLemma

fn clone(&self) -> CommittedLemma

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CommittedLemma

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

Formats the value using the given formatter.