Struct LawTheorem 

pub struct LawTheorem {
    pub fn_id: FnId,
    pub law_name: String,
    pub quantifiers: Vec<Quantifier>,
    pub premises: Vec<Predicate>,
    pub claim_lhs: Spanned<ResolvedExpr>,
    pub claim_rhs: Spanned<ResolvedExpr>,
    pub strategy: ProofStrategy,
}

Lowered verify-law theorem. All projection decisions (.val vs bare ident, wrapper strip, when-keep vs when-drop) are already baked into the fields below; backends render directly.

Fields

fn_id: FnId

Opaque identity of the fn this law targets, resolved through SymbolTable at populate time (phase E3). Verify laws are entry-only per the current model, so this is effectively always an entry-scope FnId today; once laws-in-modules lands the same FnId will distinguish two same-bare-name recursive fns across modules without any per-callsite scope plumbing.

law_name: String

quantifiers: Vec<Quantifier>

premises: Vec<Predicate>

Premises in order. Already includes when if it carries information beyond the refinement invariants (the lowerer performs the bijective syntactic equivalence check).

claim_lhs: Spanned<ResolvedExpr>

LHS = RHS claim. Wrapper-stripped, lifted-var-aware (bare idents for arg positions, .val projections inside comparator BinOps if the lowerer determined this is needed).

claim_rhs: Spanned<ResolvedExpr>

strategy: ProofStrategy

Trait Implementations

impl Clone for LawTheorem

fn clone(&self) -> LawTheorem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LawTheorem

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

Formats the value using the given formatter.