Struct InductionCase 

pub struct InductionCase {
    pub constructor: String,
    pub args: Vec<InductionArg>,
}

The “Lever” - The specific logical move made at each proof step.

This enum captures HOW we moved from premises to conclusion. Each variant corresponds to a different proof strategy or logical rule.

See Also

• DerivationTree - Each node contains an InferenceRule
• certifier::certify - Maps inference rules to kernel terms
• hints::suggest_hint - Suggests applicable rules when stuck
• BackwardChainer - The engine that selects and applies rules

One constructor’s case in a generic induction scheme (InferenceRule::InductionScheme). The derivation’s premises align 1:1 with the cases, in the inductive’s constructor-registration order.

Fields

constructor: String

The constructor this case eliminates (e.g. "Succ", "Node").

args: Vec<InductionArg>

The constructor’s arguments, in order — each bound in the case body.

Trait Implementations

impl Clone for InductionCase

fn clone(&self) -> InductionCase

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InductionCase

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

Formats the value using the given formatter.

impl PartialEq for InductionCase

fn eq(&self, other: &InductionCase) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for InductionCase